Resolution inference
In propositional logic, a resolution inference is an instance of the following rule:
We call:
This rule can be generalized to first-order logic to:
where is a most general unifier of and and and have no common variables.Example
The clauses and can apply this rule with as unifier.
Here x is a variable and b is a constant.
Here we see that
- The clauses and are the inference’s premises
- is its conclusion.
- The literal is the left resolved literal,
- The literal is the right resolved literal,
- is the resolved atom or pivot.
- is the most general unifier of the resolved literals.
