

Introduction to Logic

Tools for Thought


As with Propositional Logic, we can use a test for unsatisfiability to test logical entailment as well. Suppose we wish to show that the set of sentences Δ logically entails the formula φ. We can do this by finding a proof of φ from Δ, i.e. by establishing Δ  φ. By the refutation theorem, we can establish that Δ  φ by showing that Δ∪{¬φ} is unsatisfiable. Thus, if we show that the set of formulas Δ∪{¬φ} is unsatisfiable, we have demonstrated that Δ logically entails φ.

To apply this technique of establishing logical entailment by establishing unsatisfiability using resolution, we first negate φ and add it to Δ to yield Δ'. We then convert Δ' to clausal form and apply resolution. If the empty clause is produced, the original Δ' was unsatisfiable, and we have demonstrated that Δ logically entails φ. This process is called a resolution refutation ; it is illustrated by examples in the following sections.

As an example of using Resolution to determine logical entailment, let's consider a case we saw earlier. The premises are shown below. We know that everybody loves somebody and everybody loves a lover.
∀x.∃y.loves(x,y)
∀u.∀v.∀w.(loves(v,w) ⇒ loves(u,v))

Our goal is to show that everybody loves everybody.
∀x.∀y.loves(x,y)

In order to solve this problem, we add the negation of our desired conclusion to the premises and convert to clausal form, leading to the clauses shown below. Note the use of a Skolem function in the first clause and the use of Skolem constants in the clause derived from the negated goal.
{loves(x,f(x))}
{¬loves(v,w), loves(u,v)}
{¬loves(a,b)}


Starting from these initial clauses, we can use resolution to derive the empty clause and thus prove the result.
1.  {loves(x,f(x))}  Premise 
2.  {¬loves(v,w), loves(u,v)}  Premise 
3.  {¬loves(a,b)}  Premise 
4.  {loves(u, x)}  1, 2 
5.  {}  4, 3 

As another example of resolution, once again consider the problem of Harry and Ralph introduced in the preceding chapter. We know that every horse can outrun every dog. Some greyhounds can outrun every rabbit. Greyhounds are dogs. The relationship of being faster is transitive. Harry is a horse. Ralph is a rabbit.
∀x.∀y.(h(x) ∧ d(y) ⇒ f(x, y))
∃y.(g(y) ∧ ∀z.(r(z) ⇒ f(y, z)))
∀y.(g(y) ⇒ d(y))
∀x.∀y.∀z.(f(x, y) ∧ f(y, z) ⇒ f(x, z))
h(harry)
r(ralph)

We desire to prove that Harry is faster than Ralph. In order to do this, we negate the desired conclusion.
¬f(harry, ralph)

To do the proof, we take the premises and the negated conclusion and convert to clausal form. The resulting clauses are shown below. Note that the second premise has turned into two clauses.
1.  {¬h(x), ¬d(y), f(x, y)}  Premise 
2.  {g(gary)}  Premise 
3.  {¬r(z), f(gary, z)}  Premise 
4.  {¬g(y), d(y)}  Premise 
5.  {¬f(x, y), ¬f(y, z), f(x, z)}  Premise 
6.  {h(harry)}  Premise 
7.  {r(ralph)}  Premise 
8.  {¬f(harry, ralph)}  Negated Goal 

From these clauses, we can derive the empty clause, as shown in the following derivation.
9.  {d(gary)}  2, 4 
10.  {¬d(y), f(harry, y)}  6, 1 
11.  {f(harry, gary)}  9, 10 
12.  {f(gary, ralph)}  7, 3 
13.  {¬f(gary, z), f(harry, z)}  11, 5 
14.  {f(harry, ralph)}  12, 13 
15.  {}  14, 8 

Don't be misled by the simplicity of these examples. Resolution can and has been used in proving complex mathematical theorems, in proving the correctness of programs, and in various other applications.

Use the arrow keys to navigate.
Press the escape key to toggle all / one.

