In propositional logic, a resolution inference is an instance of the following rule:
Γ
1
∪
{
ℓ
}
Γ
2
∪
{
ℓ
¯
}
Γ
1
∪
Γ
2
|
ℓ
|
We call:
The clauses
Γ
1
∪
{
ℓ
}
and
Γ
2
∪
{
ℓ
¯
}
are the inference’s premises
Γ
1
∪
Γ
2
(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:
Γ
1
∪
{
L
1
}
Γ
2
∪
{
L
2
}
(
Γ
1
∪
Γ
2
)
ϕ
ϕ
where
ϕ
is a most general unifier of
L
1
and
L
2
¯
and
Γ
1
and
Γ
2
have no common variables.
The clauses
P
(
x
)
,
Q
(
x
)
and
¬
P
(
b
)
can apply this rule with
[
b
/
x
]
as unifier.
Here x is a variable and b is a constant.
P
(
x
)
,
Q
(
x
)
¬
P
(
b
)
Q
(
b
)
[
b
/
x
]
Here we see that
The clauses
P
(
x
)
,
Q
(
x
)
and
¬
P
(
x
)
are the inference’s premises
Q
(
b
)
(the resolvent of the premises) is its conclusion.
The literal
P
(
x
)
is the left resolved literal,
The literal
¬
P
(
b
)
is the right resolved literal,
P
is the resolved atom or pivot.
[
b
/
x
]
is the most general unifier of the resolved literals.
