【正文】 Chapter 5 Information Processing and Utilization Section 3 Theorem Proving 1. Terminology 1) Atom A proposition/predicate that can not be deposed into other proposition/predicate is an atom. 2) Literal Atom and the negated atom are called literals. 3) Clause A number of literals connected only by disjunctive symbols are called clauses. 4) Term Constant, variable, function are called terms. 5) Well formed formula (wff) Any legal expressions/formulas are called wffs. 6) An interpretation of a formula is an assignment of a truth value to every atom of the formula. A formula containing n distinct atoms has 2 distinct interpretations. Under each interpretation, a formula can be evaluated to be true or false. 7) An interpretation is said to satisfy a formula iff it can make the formula true . 8) A formula is valid iff true under all its interpretations 9) A formula is inconsistency iff it is false under all its interpretations. 10) A formula is consistent iff it is not inconsistent. A consistent formula is true under at least one interpretation. n 11) Formula G is said to be a logical consequence of formulas F1, …, Fn iff every interpretation that satisfies (F1∧ F2∧ ... ∧ Fn) also satisfies G. 12) Rules of inference are operations, in the logic, which can be applied to certain Wffs and sets of Wffs to produce new Wffs. Modus Ponens: P(x), P(x) →Q(x) ? Q(x) Universal Specialization: (?x)P(x), A ? P(A) 13) Theorems: Wffs as a logic consequence derived from ones by inference rules applications. 14) Proof of a theorem: The sequence of inference rules applications used in new Wffs derivation. 2. Preliminary Knowledge (a) Unification: process of finding substitutions, {s}, of terms for variables, {t/v}, to make expressions identical. A substitution instance of an expression E is obtained by substituting terms for variables in that expression and denoted by Es. A set of expressions {Ei} is said unifiable if there exists a substitution s such that E1s = E2s = … = Ens, and s is said to be a unifier of {Ei}. The most general (simplest) unifier of {Ei} is denoted by mgu. (b) Process for Conversion of Wff to Clause Form (1) Eliminate implication symbols (2) Reduce scopes of negation symbols (3) Standardize variables (4) Eliminate existential quantifiers (5) Convert to prenex form (6) Put matrix in conjunctive normal form (7) Eliminate universal quantifiers (8) Eliminate conjunction symbols (9) Rename variables 3. Resolution Principle (RP) (a) Concept: RP is a procedure that produces proofs by refutation. To prove a statement, RP attempts to show that the negation of the statement produces a contradiction with the known statement. (b) RP in Propositional Logic Given premises S and a conclusion G to be proved. (1) Convert all the propositions of S to clause form. (2) Negate G and then convert into clause form, add it to the set of clauses obtained in (1). (3) Repeat until either a contradiction is found or no progress can be made: (a) Select two clauses c and c , the parent clauses. (b) Resolve c and c , the resulting clause, called the resolvent, r , will be the disjunction of all the literals of both the parent clauses with the following exception: If there are any pair of literal L and ?L, such that one of the parent clauses contains L and the other contain ?L, then delete L and ?L from the resolvent. (c) If the resolvent is the empty clause, NIL, then a contradiction has been found. If it is not, then add it to the set of clauses available to the procedure. i j ij i i j j Examples 1: Parent Clauses Resolvent p?l?m? …, ?p?n?o? … l ?m?n?o?… p, ?p?q q (MP) p?q, ?p?q q?q = q (Merge) p?q, ? p?? q q??q, p? ?p (Taotology) ?p, p NIL (Empty) ?p?q, ?q?r ?p?r (chaining) Example 2: Given Premises Convert to Clause Form p p (1) (p?q)?r ? p? ? q? r (2) (s?t) ?q ? s ? q (3) ? t ? q (4) Conclusion: t t (5) Negated Goal ? r (6) RP: (2,6) ? p ? ? q (7) (1,7) ? q (8) (4,8) ? t (9) (5,9) NIL (10) This is a contradiction among the premises and the negated conclusion. The premises are known valid. Therefore the invalid ponent must be the negated conclusion. In other words, the conclusion should be the logic consequence of the premises. 4. RP in Predicate Logic Given: a set of premises S and a conclu