|
|
Introduction to Logic
|
Tools for Thought
|
|
As with Propositional Resolution, Resolution works only on expressions in clausal form. The definitions here are analogous. A literal is either a relational sentence or a negation of a relational sentence. A clause is a set of literals and, as in Propositional Logic, represents a disjunction of the literals in the set. A clause set is a set of clauses and represents a conjunction of the clauses in the set.
|
The procedure for converting relational sentences to clausal form is similar to that for Propositional Logic. Some of the rules are the same. However, there are a few additional rules to deal with the presence of variables and quantifiers. The conversion rules are summarized below and should be applied in order.
|
In the first step (Implications out), we eliminate all occurrences of the ⇒, ⇐, and ⇔ operators by substituting equivalent sentences involving only the ∧, ∨, and ¬ operators.
φ ⇒ ψ | → | ¬φ ∨ ψ |
φ ⇐ ψ | → | φ ∨ ¬ψ |
φ ⇔ ψ | → | (¬φ ∨ ψ) ∧ (φ ∨ ¬ψ) |
In the second step (Negations in), negations are distributed over other logical operators and quantifiers until each such operator applies to a single atomic sentence. The following replacement rules do the job.
¬¬φ | → | φ |
¬(φ ∧ ψ) | → | ¬φ ∨ ¬ψ |
¬(φ ∨ ψ) | → | ¬φ ∧ ¬ψ |
¬∀ν.φ | → | ∃ν.¬φ |
¬∃ν.φ | → | ∀ν.¬φ |
|
In the third step (Standardize variables), we rename variables so that each quantifier has a unique variable, i.e. the same variable is not quantified more than once within the same sentence. The following transformation is an example.
∀x.(p(x) ⇒ ∃x.q(x)) |
→ |
∀x.(p(x) ⇒ ∃y.q(y)) |
|
In the fourth step (Existentials out), we eliminate all existential quantifiers. The method for doing this is a little complicated, and we describe it in two stages.
If an existential quantifier does not occur within the scope of a universal quantifier, we simply drop the quantifier and replace all occurrences of the quantified variable by a new constant; i.e., one that does not occur anywhere else in our database. The constant used to replace the existential variable in this case is called a Skolem constant. The following example assumes that a is not used anywhere else.
If an existential quantifier is within the scope of any universal quantifiers, there is the possibility that the value of the existential variable depends on the values of the associated universal variables. Consequently, we cannot replace the existential variable with a constant. Instead, the general rule is to drop the existential quantifier and to replace the associated variable by a term formed from a new function symbol applied to the variables associated with the enclosing universal quantifiers. Any function defined in this way is called a Skolem function.
∀x.(p(x) ∧ ∃z.q(x, y, z)) |
→ |
∀x.(p(x) ∧ q(x, y, f(x, y))) |
|
In the fifth step (Alls out), we drop all universal quantifiers. Because the remaining variables at this point are universally quantified, this does not introduce any ambiguities.
∀x.(p(x) ∧ q(x, y, f(x, y))) |
→ |
p(x) ∧ q(x, y, f(x, y)) |
In the sixth step (Disjunctions in), we put the expression into conjunctive normal form, i.e. a conjunction of disjunctions of literals. This can be accomplished by repeated use of the following rules.
φ ∨ (ψ ∧ χ) | → | (φ ∨ ψ) ∧ (φ ∨ χ) |
(φ ∧ ψ) ∨ χ | → | (φ ∨ χ) ∧ (ψ ∨ χ) |
φ ∨ (φ1 ∨ ... ∨ φn) | → | φ ∨ φ1 ∨ ... ∨ φn |
(φ1 ∨ ... ∨ φn) ∨ φ | → | φ1 ∨ ... ∨ φn ∨ φ |
φ ∧ (φ1 ∧ ... ∧ φn) | → | φ ∧ φ1 ∧ ... ∧ φn |
(φ1 ∧ ... ∧ φn) ∧ φ | → | φ1 ∧ ... ∧ φn ∧ φ |
|
In the seventh step (Operators out), we eliminate operators by separating any conjunctions into its conjuncts and writing each disjunction as a separate clause.
φ1 ∧ ... ∧ φn | → | φ1 |
| → | ... |
| → | φn |
φ1 ∨ ... ∨ φn | → | {φ1, ... , φn} |
|
As an example of this conversion process, consider the problem of transforming the following expression to clausal form. The initial expression appears on the top line, and the expressions on the labeled lines are the results of the corresponding steps of the conversion procedure.
| ∃y.(g(y) ∧ ∀z.(r(z) ⇒ f(y, z))) |
I | ∃y.(g(y) ∧ ∀z.(¬r(z) ∨ f(y, z))) |
N | ∃y.(g(y) ∧ ∀z.(¬r(z) ∨ f(y, z))) |
S | ∃y.(g(y) ∧ ∀z.(¬r(z) ∨ f(y, z))) |
E | g(gary) ∧ ∀z.(¬r(z) ∨ f(gary, z)) |
A | g(gary) ∧ (¬r(z) ∨ f(gary, z)) |
D | g(gary) ∧ (¬r(z) ∨ f(gary, z)) |
O | {g(gary)} |
| {¬r(z), f(gary, z)} |
|
Here is another example. In this case, the starting sentence is almost the same. The only difference is the leading ¬, but
the result looks quite different.
| ¬∃y.(g(y) ∧ ∀z.(r(z) ⇒ f(y, z))) |
I | ¬∃y.(g(y) ∧ ∀z.(¬r(z) ∨ f(y, z))) |
N | ∀y.(¬(g(y) ∧ ∀z.(¬r(z) ∨ f(y, z))) |
| ∀y.(¬g(y) ∨ ¬∀z.(¬r(z) ∨ f(y, z))) |
| ∀y.(¬g(y) ∨ ∃z.¬(¬r(z) ∨ f(y, z))) |
| ∀y.(¬g(y) ∨ ∃z.(¬¬r(z) ∧ ¬f(y, z))) |
| ∀y.(¬g(y) ∨ ∃z.(r(z) ∧ ¬f(y, z))) |
S | ∀y.(¬g(y) ∨ ∃z.(r(z) ∧ ¬f(y, z))) |
E | ∀y.(¬g(y) ∨ (r(k(y)) ∧ ¬f(y, k(y)))) |
A | ¬g(y) ∨ (r(k(y)) ∧ ¬f(y, k(y))) |
D | (¬g(y) ∨ r(k(y))) ∧ (¬g(y) ∨ ¬f(y, k(y))) |
O | {¬g(y), r(k(y))} |
| {¬g(y), ¬f(y, k(y))} |
|
In Propositional Logic, the clause set corresponding to any sentence is logically equivalent to that sentence. In Relational Logic, this is not necessarily the case. For example, the clausal form of the sentence ∃x.p(x) is {p(a)}. This is not logically equivalent. It is not even in the same language. Since the clause exists in a language with an additional object constant, there are truth assignments that satisfy the sentence but not the clause. On the other hand, the converted clause set has a special relationship to the original set of sentences: over the expanded language, the clause set is satisfiable if and only if the original sentence is satisfiable (also over the expanded language). As we shall see, in resolution, this equivalence of satisfiability is all we need to obtain a proof method as powerful as the Fitch system (without Domain Closure or Induction).
|
Use the arrow keys to navigate.
Press the escape key to toggle all / one.
|
|