Resolution inference
From Wikipedia, the free encyclopedia
In propositional logic, a resolution inference is an instance of the following rule:[1]
We call:
- The clauses
and
are the inference’s premises
(the resolvent of the premises) is its conclusion.
- The literal
is the left resolved literal,
- The literal
is the right resolved literal,
is the resolved atom or pivot.
This rule can be generalized to first-order logic to:[2]
where is a most general unifier of
and
and
and
have no common variables.
Example[edit]
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
(the resolvent of the 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.