Back to Confucius case

In this section we shall give a few examples to illustrate some applications of the first-order logic to problem solving. As in the prepositional logic, the usual approach is first to symbolize problems by formulas and then to prove that the formulas are valid or inconsistent.

Ex. There are two premises:

F₁: (∀x)(MAN (x)→MORTAL(x));

F₂:MAN(Conf).

Prove that G: MORTAL(Conf) logically follows from F₁ and F₂.

Solution:

F₁ʌF₂ʌ~G = (∀x)(MAN(x)→MORTAL(x))ʌMAN(Conf)ʌ~MORTAL(Conf); (It is PNF.) We just eliminate the universal quantifier to obtain the matrix.

Matrix = (MAN(x)→MORTAL(x)) ʌ MAN(Conf) ʌ ~MORTAL(Conf);

CNF = (~MAN(x) v MORTAL(x)) ʌ MAN(Conf) ʌ ~MORTAL(Conf);

Set of clauses:

1. ~MAN(x) v MORTAL(x)

2. MAN(Conf) ~MAN(Conf) [unify: x = Conf]

3. ~MORTAL(Conf)

4. ~MAN(Conf) empty clause

5. Empty clause

Resolution Proof

1.Resolve 3 and 1, specializing (= substituting, “unifying”) x to Conf.

Add MORTAL(Conf) as clause#4 available for further resolutions.

2. Resolve 4 and 2 to get an empty clause. Add it to the set of clauses. The contradiction in reasoning is found. Assumption ~MORTAL(Conf) is FALSE. Hence, MORTAL(Conf) = TRUE.

Note: In the set of clauses1, 2, 3, each clause is supposed to be true. We generated some more clauses using resolution which is a sound inference rule. We came to impossible situation: ~MAN(Conf) and MAN(Conf) are both generated as true. An empty clause is the indication on the contradiction. The premises are true for sure. The source of contradiction is clause #3.