【正文】 raph having a leaf node, n, labeled by literal L. The result is a new AND/OR graph in which node n now has an outgoing 1connector to a descendant node (also label by L) which is the root node of that AND/OR graph structure representing W. ., S ? (x ? y) ? z is applied to T U T? U S S? (T? U) L S? (T? U) T? U T U S S Z Y X X ? Y L L Match Arc W From the rule L ? W and the fact expression F(L), the expression F(W) can be derived from F(L) by replacing all the occurrences of L in F by W, and thus a new graph containing a representation of F(W) is produced. After a rule is applied at leaf node, this node is no longer a leaf node of the graph, but it is still labeled by a single literal and may continue to have rules applied to it. Any node labeled by a single literal is called a literal node. The set of clauses represented by an AND/OR graph is the set that corresponds to the set of solution graph terminating in literal nodes of the graph. Termination of Rule Applications The object of the forward production system is to prove some goal wff from fact wffs and a set of rules. Hence, whenever the goal wff is reached, the system can be terminated. The forward system is limited in proving those goal wffs whose form is disjunction of literals. When one of the goal literals matched a literal node, n, of the AND/OR graph, we add a new descendant of node n, labeled by the matching goal literal, to the graph. This descendant is called a goal node. ., C D A A ? B B B G E G A C Fact: A ? B Rules: A ? C ? D B ? E ? G Goal: C ? G Rule Matching Goal Matching (C) Rule Application in Predicate Logic Fact and rule expressions are the same as above: Variables are universally quantified。 * Variables within the scopes of universal quantifiers are standardized by renaming: variables in different conjunctions have different names。 utilization Section 4 RuleBased Deduction Systems 1. Introduction Rulebased Deduction Systems do not convert wffs to clause forms as the latter forms would lose information: A? B ? C = ? (A? B) ? C = ? (A ? C) ? B = … Wffs representing assertion knowledge are separated into two categories: (1) The rules expressed in implication form。 R) 8. NIL (7, 3a。 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