Chapter 9: Inference in first order logic SUBST(b, φ) : the result of applying the substition b to the sentence φ. b is a binding list example : SUBST({x/Sam, y/Pam}, Likes(x,y)) = Likes(Sam, Pam) Inference rule : 1. Universal elimination : $v φ => SUBST({v, g}, φ) where g is any ground term. 2. Existential elimination : #v φ => SUBST({v, k}, φ) where k is a constant symbol that does not appear elsewhere. 3. Existential Introduction : φ => #v SUBST({g/v}, φ) where g is a ground term, v is a variable. Generalized Modus Ponens if SUBST(theta, pi')=SUBST(theta, pi) then p1',p2', ...,pn', (p1&p2&...&pn=>q) => SUBST(theta, q) Horn Sentence Unification UNIFY(p, q) = theta if SUBST(theta, p)=SUBST(theta, q) where the UNIFY return the Most General Unifier (MGU) example: UNIFY(Knows(John, x), Knows(y, z)) may have {y/John, x/z}, {y/John, x/John, z/John}... but {y/John, x/z} use the least commitment Forward Chaining Algorithm ( is a data-driven (data-directed) procedure) Renaming : Likes(x, IceCream) = Likes(y, IceCream) Composition : COMPOSE(theta1, theta2) SUBST(COMPOSE(theta1, theta2), p) = SUBST(theta2, SUBST(theta1, p)) procedure FORWARD-CHAIN(KB, p) if there is a sentence in KB that is a renaming of p then return Add p to KB // 新加入一條 fact, 盡可能的去觸發所有可能的 unification. for each (p1&...&pn=>q) in KB such that for some i, UNIFY(pi, p)= theta succeeds do FIND-AND-INFER(KB, [p1,...,Pi-1,Pi+1,...Pn], q, theta) end procedure FIND-AND-INFER(KB, premoses, concolusion, theta) if premise = [] then // 本規則完全 unify 成功, 把 conclusion 也加入, 並看能否進一步觸發其它規則. FORWARD-CHAIN(KB, SUBST(theta, conclusion)) else for each p' in KB such that UNIFY(p', SUBST(theta, FIRST(premises))) = theta2 do // 把可以 unify 的規則一直 unify 到無法 unify 為止. FIND-AND-INFER(KB, REST(premise), conclusion, COMPOSE(theta, theta2)) end function BACK-CHAIN(KB, q) returns a set of substitutions BACK-CHAIN-LIST(KB, [q], {}) function BACK-CHAIN-LIST(KB, qlist, theta) returns a set of substitutions input : KB, a knowledge base qlist, a list of conjuncts forming a query (theta already applied) theta, the current substitution local variables : answers, a set of substitutions, initially empty if qlist is empty then return {theta} q = FIRST(qlist) for each qi' in KB such that theta i = UNIFY(qi, qi') succeeds do Add COMPOSE(theta, theta i) to answer end for each sentence (p1&...&pn=>qi') in KB such that theta i = UNIFY(q, q') succeeds do answers = BACK-CHAIN-LIST(KB, SUBST(theta i, [p1,...,pn]), COMPOSE(theta, theta i)) ∪ answers end return the union of BACK-CHAIN-LIST(KB, REST(qlist), theta) for each theta in answers. KB : American(x) & Weapon(y) & Nation(z) & Hostile(z) & Sells(x, z, y) => Criminal(x) Owns(Nono, x) & Missile(x) => Sells( West, Nono, x) Missile(x) => Weapon(x) Enemy(x, America ) => Hostile(x) FACTS : American(West) Nation(Nono) Enemy(Nono, America) Owns(Nono, M1) Missile(M1) Forward chaining example {American(West)} & Weapon(y) & Nation(z) & Hostile(z) & Sells(West, z, y) => Criminal(West) {Nation(Nono)} & American(x) & Weapon(y) & Hostile(z) & Sells(x, z, y) => Criminal(x) {American(West) & Nation(Nono)} & Weapon(y) & Hostile(Nono) & Sells(x, z, y) => Criminal(West) {Enemy(Nono, America)} ... => Hostile(Nono) {American(West) & Nation(Nono) & Hostile(Nono)} & Weapon(y) & Sells(West, Nono, y) => Criminal(West) {Owns(Nono, M1) } & Missile(M1) => Sells( West, Nono, M1) {Owns(Nono, M1) , Missile(M1) } ... => Sells(West, Nono, M1) {American(West) & Nation(Nono) & Hostile(Nono) & Sells(West, Nono, M1) } & Weapon(y) => Criminal(West) { Missile(M1) } ...=> Weapon(M1) {American(West) & Nation(Nono) & Hostile(Nono) & Sells(West, Nono, M1) & Weapon(M1)} ...=> Criminal(West) question sentence found. Backward chaining example ? Criminal(West):?American(West)&?Weapon(y)&?Nation(z)&?Hostile(z)&?Sells(West, z, y): yes ? American(West) : yes-^ ^ ^ ^ ^ ? Weapon(y) : ? Missile(y) : Missile(M1) {y/M1} | | | ? Nation(z) : Nation(Nono) {z/Nono}-------------+ | | ? Hostile(Nono) : yes-----------------------------------------+ | ? Sell(West, Nono, M1) : yes -------------------------------------------+ Forward chaining and Backward chaining is not complete Proof : In Case Analysis KB : $x P(x) => Q(x) $x -P(x)=> R(x) $x Q(x) => S(x) $x R(x) => S(x) --------------- KB ╞ $x S(x) but KB !╞ $x S(x) in Forward chaining and Backward chaining. Complete : if KB╞φ then KB ├ φ by Resolution Procedure Resolution in and/or form (a|b) & (-b|c) => a|c Resolution in implication form (-a=>b & b=>c) => -a=>c Generalized Resolution in and/or form [p] = [p1|...pj...|pm] [q] = [q1|...qk...|qn] [p] &[q] => SUBST(theta, [p]-pj, [q]-qk) where UNIFY(pj, -qk) = theta Generalized Resolution in implication form [p] = [p1&...pj...&pn1] [r] = [r1|........|rn2] [s] = [s1&........&sn3] [q] = [q1|...qk...|qn4] (([p] => [r]) & ([s] => [q])) => SUBST(theta, (([p]-pj)&[s])=>([r]|([q]-qk)))) (where UNIFY(pj, -qk) = theta ) Canonical form for resolution : Conjunctive normal form (CNF) -P(w)|Q(w) P(x)|R(x) -Q(y)|S(y) -R(z)|S(z) Implicative Normal Form (INF) P(w)=>Q(w) True=>P(x)|R(x) Q(y)=>S(y) R(z)=>S(z) P(w)=>Q(w) Q(y)=>S(y) \ {y/w} / P(w)=>S(w) True=>P(x)|R(x) \ {w/x} / True=>S(x)|R(x) R(z)=>S(z) \ {x/A,z/A} / True=>S(A) S(A)=>False \ / True=>False -P(w)|Q(w) -Q(y)|S(y) \ {y/w} / -P(w)|S(w) P(x)|R(x) \ {w/x} / S(x)|R(x) -R(z)|S(z) \ {x/A,z/A} / S(A) -S(A) \ / FALSE Conversion to Normal Form Eliminate implication (p=>q) ├ (-p|q) Move - inwards -(p|q) ├ (-p&-q) -(p&q) ├ (-p|-q) -($x,p)├ (#x -p) --p ├ p Standardize variables rename variable in different scope with different name. Move quantifiers left p|$x q ├ $x p|q Skolemize : removing # by elimination. $x Person(x) => #y Heart(y)&Has(x, y) ->$x Person(x) => Heart(F(x))&Has(x, F(x)) Distribute & over | : (a&b)|c -> (a|c)&(b|c) Flatten nested conjunctions and disjunctions : (a|b)|c -> (a|b|c) Convert disjunctions to implications (-a|-b|c|d) -> (a&b=>c|d) Example Proof : In implication normal form : Axiom : #x Dog(x)&Own(Jack, x) $x(#y Dog(y)&Own(x, y))=>AnimalLover(x)) $x(AnimalLover(x)=>($y -Animal(y)=>-Kill(x,y))) $x(Cat(x)=>Animal(x)) Dog(D) Own(Jack, D) Cat(Tuna) Kills(jack, Tuna)|Kills(Curiosity, Tuna) In implication form: $x(#y Dog(y)&Own(x, y))=>AnimalLover(x)) Dog(F1[x]) $x$y(AnimalLover(x)=>(Animal(y)=>-Kill(x,y))) $x(Cat(x)=>Animal(x)) Dog(D) Own(Jack, D) Cat(Tuna) Kills(Jack, Tuna)|Kills(Curiosity, Tuna) Dog(D) Dog(y)&Own(x, y)=>AnimalLover(x) \ / {y/D} Own(x, D)=>AnimalLover(x) Own(Jack, D) {x/Jack} \ / AnimalLover(x)=>(-Animal(y)=>-Kill(x, y)) AnimalLover(Jack) \ / Cat(Tuna) Cat(x)=>Animal(x) Animal(y)=>-Kill(Jack, y) \ / / Animal(Tuna) / \ / -Kill(Jack, Tuna) Kills(Jack, Tuna)|Kills(Curiosity, Tuna) \ / Kill(Curiosity, Tuna) -Kill(Curiosity, Tuna) \ / False In conjunction normal form : -Dog(y)|-Own(x, y)|AnimalLover(x) Dog(F1[x]) -AnimalLover(x)|-Animal(y)|Kill(x,y) -Cat(x)|Animal(x) Dog(D) Own(Jack, D) Cat(Tuna) Kills(Jack, Tuna)|Kills(Curiosity, Tuna) Dog(D) -Dog(y)|-Own(x, y)|AnimalLover(x) \ / {y/D} -Own(x, D)|AnimalLover(x) Own(Jack, D) {x/Jack} \ / -AnimalLover(x)|-Animal(y)|Kill(x, y) AnimalLover(Jack) \ / Cat(Tuna) -Cat(x)|Animal(x) -Animal(y)|Kill(Jack, y) \ / / Animal(Tuna) / \ / -Kill(Jack, Tuna) Kills(Jack, Tuna)|Kills(Curiosity, Tuna) \ / Kill(Curiosity, Tuna) -Kill(Curiosity, Tuna) \ / False Dealing with equality A=B & P(A) cannot unify with P(B), it’s unreasonable. Method 1 : Axiomize equality $x x=x $x,y x=y => y=x $x,y,z x=y & y=z => x=z $x,y x=y => (P1(x)<=>P1(y)) .. .. $w,x,y,z w=y&x=z => (F(w,x)=F(y,z)) .. .. Method 2 : Demodulation UNIFY(x,z)= theta & x=y, (.. z .. ) => (.. SUBST(theta, y) ..) Resolution strategy Unit preference (Wos 1964): 短者優先 Set of support (Wos 1965): 1. identify set of support 2. combine(x,y) x in set of support, y in KB Input resolution : combine(x,y) x is input sentence, y in KB In Horn clause , input resolution is complete. Linear resolution (Loveland 1968): if P=>..=>Q then Q, Q then Unify(P,z), Unify(Q,z) should be done together. Subsumption : eliminates all sentences that are subsumed by an existing sentence in the KB. Example : if P(x) in KB then P(A) should be deleted from axiom.

Chapter 7: First order logic Constant + Predicate + Function = First Order Logic Term : Constant , variable or Function Ground Term : A term with no variable Atomic Sentence : Predicate with parameter. Complex Sentence : Sentence with logical connective. Quantifier : $, #, #!, Second Order Logic : $p φ Situation calculus : 1. Special time sequence variable called situation : S0,S1,S2,.. , St, … 2. Result(action, Si)=Si+1 3. Effect axiom : axioms that make the world change. Ex: -Hold(x, Result(Release, s)) 4. Frame axioms : axioms that describe how the world stay the same. Ex: -Hold(x,s)^(a≠Grab├(Present(x,s)^Portable(x))=>-Hold(x,Result(a,s)) 5. Successor-state axiom = Effect axiom + Frame axiom Ex: Hold(x,Result(a,s)) <=>[(a=Grab^Present(x,s)^Portable(x))|(Hold(x,s)^a≠Release)] Representational Frame Problem : The proliferation of frame axioms (solved by Successor-state axiom) Inferential Frame Problem : When reasoning about the result or a long sequence of action in situation calculus, we have to carry each property through all intervening situation one step at a time, even if the property remain unchanged throughout.(this is why that special purpose reasoning system such as planning system is needed). Qualification : it’s difficult to define the circumstances under which a given action is guaranteed to work. Ramification Problem : it’s almost impossible to describe all the implicit consequence of actions. Deduce Hidden Properties of the World Synchronic rules : relate properties of a world property of the world causes certain percepts to be generated. (Type1) Causal rules : Conclusion => Environment (Type2) Diagnostic rules : Percept => Conclusion

Chapter 5: First Order Logic Syntax : Vocabulary : Σ = (Φ, π, r) Φ : a set of function symbol π : a set of relation symbol r : Φ ∪ π --> N , arity function Remark1 : if f in Φ and r(f) = 0 then f is called a constant Remark2: We can treat Boolean logic as a special case of first order logic, in which Φ = empty and r(p) = 0 for all p in π Remark3: The text book require the arity of a relation symbol cannot be 0, in which case lemma 2 does not apply. V = {x, y, z, ... } , a countably infinite set of variable T(Φ, V) : set of terms (1) V in T(Φ, V) (2) if f in Φ , r(f) = k and t1... tk in T(Φ, V) then f(t1...tk) in T(Φ, V) A(Φ, π, V) : set of atomic expression if p in π, r(p) = k, t1...tk in T(Φ, V) then p(t1...tk) in A(Φ, π, V) F(Φ, π, V) : set of first order expression(first order formulas) (1) A(Φ, π, V) in F(Φ, π, V) (2) if φ, ψin F(Φ, π, V) then -φ, φ|ψ, φ  ψin F(Φ, π, V) (3) if φ in F(Φ, π, V) and x in V then x φ, x φin F(Φ, π, V) f(x)|g(x) is wrong P(f(x))|Q(g(x)) is correct. Model Theory of First Order Logic : Given Σ a model appropriate to Σ is a pair of M = (U, μ) where U ≠ Empty U : universe of M μ: V-> U , for every variable we assign an interpretation X(μ) for every function f in Φ of arity k , μ assign a function f(μ): Uk->U for every predicate P in π of arity k, μ assign a set of k tuple Pk in Uk Given formula Φin F(Φ, π, V) μ satisfied Φ iff (1) Φ is an atom P(t1,…,tn) and <t1M…tnM> in PM Example : M satisfied P(a,x) if aM=0 , xM=3, PM = {<x,y>; x < y} (2) Φ IS -P and M satisfied P (3) Φ is P&Q and M satisfied P and M|=Q Φ is P|Q and M satisfied P or M|=Q Φ is P=>Q and M not satisfied P and M|=Q (4) Φ is X P and for every u in U μ(x=u) |= P Φ is X P and there is a u in U s.t. μ(x=u) |= P Given M, u in U definedμM(x=u)=u Proposition : let P be an expression, and M as M' be two model s.t. they differ only on variables in P, then M|=P iff M'|=P Remark : when consider the satisfiability or validity of sentence we do not need to worry about how the variable are interpreted in the model. A sentence is valid if it is true in all models. A sentence is unsatisfiable if it is not true in any model. Theorem : there is a model N' s.t. for all sentence P expressible in the language of number theory , N|=P iff N'|=P Remark : Axiomitization (N cannot be axiomitization by the language of N, but G, N mod p can ) Proof Theory : Axiom 0 : tautulogies Axiom 1 : 1. t=t 2. t1 = t1' & t2=t2' &…&tn=tn'  f(t1,..,tn) = f(t1',..,tn') 3. t1 = t1' & t2=t2' &…&tn=tn' & R(t1,…,tn)  R(t1',.., tn') Axiom 2 : x PP[x=t] when t is a term Axiom 3 :P x P x is not free in P Axiom 4 : x (PQ) (x P xQ) Modus Ponens P; PQ  Q example : P(f(a), x)|Q(f(y), g(a, y)) --> ψ  P(f(a), x)|Q(f(y), g(a, y)) --> F Example : number theory Φ = {0, succ, +, *, ^ } π = { < } // recall that = is always exist Note 1 : we can use 1 as a shorthand for succ(0) Example : graph theory Φ = Empty π = {G} r(G) = 2 Undirected Graph xy G(x,y)  G(y,x) Transitivity xyG(x,y) & G(y,z)  G(x,z) A variable is free if it is not within the scope of any x or x Otherwise, x is bound A sentence is a FOE without any free variable. Theorem : For any expression φ over Σ(G), the problem φ-graph is in P Semantic : Proposition 1 : if φ is unsatisfiable (has no model) then ╞ -φ An expression is unsatisfiable iff its negation is valid. 2 : Boolean Validity : Suppose that Boolean form of an expression φ is a tautology, then φ is valid. 3 : Equality : (t1=t1' & ... & tk = tk') => f(t1,...,tk)=f(t1',...,tk') (t1=t1' & ... & tk = tk') => R(t1,...,tk)=R(t1',...,tk') 4 : Quantifiers : 4.1 Any expression of the form φ => φ[x<-t] is valid. 4.2 If φ is valid, then so is xφ 4.3 If x does not appear free in φ, then φ => x φ is valid. 4.4 For all φ and ψ, (x (φ=>ψ)) => ((x φ)=> (x ψ)) Hilbert Style Proof Theory 1. Axioms : AX0: Any expression whose boolean form is a tautology. example : x P(x) => x P(x) , its boolean form (A=>A) is a tatulogy. x P(x) => P(X), has no exact boolean form. AX1: AX1a: t = t for every t in T(F, x) AX1b: t1=t1'&t2=t2'&..&tn=tn' => f(t1,...,tn)=f(t1',...,tn') AX1c: t1=t1'&t2=t2'&..&tn=tn'&R(t1,...,tn)=> R(t1',...,tn') AX2: Any expression of the form x φ=>φ[x<-t] AX3: Any expression of the form φ=>x φ, with x not free in φ AX4: Any expression of the form (x (φ=>ψ))=>( xφ=> xψ) illogical 不合邏輯的 alogical 非關邏輯的 Derivation (├) given a set of expression Δ and an expression φ, Δ├φ (Δ derive φ or φ is a theorem of Δ) if there is a finite sequence of expression (φ1,..., φn) s.t : (1) φn = φ (2) For all 1≦i≦n φI in Λ ∪ Δ or j,k<i s.t φj is φk=>φi If ├φ then φ is a theorem Theoremhood : Given φ , is ├φ Theorem : Theoremhood is recursive enumerable Deductive Theorem If Δ ∪ {φ} ├ ψ then Δ ├ φ=>ψ Proof: (Induction in the length of sequence of derivation) Consider a proof of S=(φ1,...,φn) of ψ from Δ ∪ {φ} (ie : φn = ψ) Suppose that for all j<i, φ=>φj if φi in Δ ∪ Λ then φi (by hypothesis), φi=>(φ=>φi) (by axiom) so φ=>φi else // if φi not in Δ ∪ Λ then the proof include φ=>φj, φ=>(φj=>φi) (by induction hypothesis) and (φ=>φj)=>((φ=>(φj=>φi))=>(φ=>φi)) is a tautology so (φ=>(φj=>φi))=>(φ=>φi) by MP φ=>φi by MP so by induction, Δ ├{φ}=>φn(= ψ)

Chapter 6 : Agent that reason logically Syntax : Describes the possible configurations that can constitute sentences. Semantic : Determines the facts in the world to which the sentences refer. interpretation for syntax Proof theory : A set of axiom + a set of inference rule. Proper reasoning should ensure that the new configurations represent facts that actually follow from the facts that the old configurations represent. ╞ (entail) (proof by truth table) KB ╞ φ means for all case -KB|φ is always true ├ (derive) (proof by axiom and inference rule) KB ├ φ means that we can derive φ from KB by axiom and inference rule. i Sound : An inference procedure i that generates only entailed sentences is called sound or truth-preserving. !├ φ & -φ Proof : The record of operation of a sound inference procedure is called a proof (proof theory). 1. KB + {φ1...φi-1} => φi ( φn = φ ) 2. For every i≦n φi in KB or φi is an axiom. Complete : An inference procedure is complete if it can find a proof for any sentence that is entailed. if φ is valid then ├ φ (Natural language have evolved more to meet the need of communication rather than representation.) Shapir-Whorf hypothesis : the language we speak profoundly influences the way in which we think and make decision. entail Sentences -----------> Sentence ↓ ↓ Facts -----------> Fact follow (理論與世界同構) Valid sentence : (tautologies , analytic sentences) A sentence that is true under all possible interpretations in all possible worlds. Satisfiable sentence : there is some interpretation in some world for which it is true. PL : propositional logic FOL : First Order Logic TL : temporal logic PT : probability theory FL : Fuzzy logic Ontological Commitment Epistemological Commitment (What exist in the world) (What an agent believes about facts) PL = (&,|,-) + proposition true/false/unknown FOL = (&,|,-) + proposition + function + predicate true/false/unknown TL = (&,|,-) + proposition + function + predicate + times true/false/unknown PT = proposition degree of belief 0..1 FL = degree of truth degree of belief 0..1 Model : any world in which a sentence is true under a particular interpretation is called a model of the sentence under that interpretation. A sentence φ is entailed by a KB if the models of KB are all models of φ. ie : KB ╞ φ ==> ╞ KB=>φ, ie: KB=>φ is valid. Prepositional logic : Syntax : 1. A set of proportion {A, B, C,...} in this language 2. All form of P&Q, P|Q, -P (P=>Q) in this language 3. No other things is in this language Semantic : 1. P => {T, F} 2. P Q -P P&Q P|Q P=>Q F F T F F T F T T F T T T F F F T F T T F T T T A sentence is valid if it's true in all row of truth table. Proof Theory Inference rule : Modus ponens : A=>B, A --> B And Elimination : A1&A2...&An --> Ai And Introduction : A1,A2,...An --> A1&A2...&An OR Introduction : Ai --> A1|A2...|An Double Negation : --A --> A Unit Resolution : A|B, -B --> A Resolution : A|B, -B|C --> A|C implication form : -A=>B, B=>C --> -A=>C Complexity of prepositional inference : SAT problem in set NP-complete Horn sentence : P1&P2...&Pn=>Q HORN-SAT in set P Monotonically : if KB1╞A then (KB1 ∪ KB2)╞A

Proof Theory A set of axiom + A set of inference rule Δ├ φ ( Δ deduce φ, φ is a theorem of Δ) if there is a sequence of boolean expressions (φ1, .., φn) such that (1) φn is φ (2) for every i≦n, φi in Δ or φi is an axiom. Soundness : A proof theory is Sound if for every φ,├φ ==> ╞ φ Completeness : A proof theory is complete if for every φ,╞ φ==>├φ To prove soundness need to prove : 1. Axiom are sound : For every axiom φ, NIL=>φ 2. Inference are sound : MP: if ╞ X and ╞ (X=>Y) then ╞ Y Boolean Logic Syntax : Boolean variable X = {x1, x2,... , xn...} logical connectiver : &, or, -, => Boolean expression (BE) (1) Every variable is a BE (2) If a, b is BE, so is a&b, a or b, -a, a=>b (3) Nothing else is a BE Semantic : Truth assignment ==> T:X -> {T, F} (1) Given T, Boolean expression φ, (T╞ φ) (2) φ is a&b ==> T╞ a and T╞ b (3) φ is -a ==> not T╞ a (4) φ is a or b ==> T╞ a or T╞ b (5) φ is a=>b ==> T╞ -a or T╞ b (6) φ is ab ==> T╞ (a=>b) & T╞ (b=>a) φ is satisfiable if there is a T s.t T╞ φ φ is valid if T╞ φ for all T in which all variable assignment in φ // If φ is valid we also call φ a tautology φ is unsatisfiable if there is no T s.t. T╞ φ Atom : a variable Literal : an atom or it's negation Clause : a disjunction of literals Set of clauses : S = a conjunction of clauses S = {c1, c2, …, cn} = c1 & c2 & ... & cn A propositional formula is in clausal form if it is represented as a set of clauses. Every boolean formula can be expressed in clausal form. To decide if φ is valid, both Davis-Patumn method and Ground resolution convert -φ into clausal form then try to prove that it is unsatisfiable. Truth Table Proof Theory φ is valid iff T╞ φ for the 2^n truth assignment in which validity the n variable of φ appear Hilbert style proof theory : (logical induction system) Axiom : (1) a=>(a=>a) (2) a=>(b=> a&b) (3) a&b =>a (4) a&b =>b (5) a=> a or b (6) b=> a or b (7) (a or b) => ((a=>r)=>((a=>b)=>r)) (8) (a=>b) => ((a=>(b=>r))=>(a=>r)) (9) (a=>b) => ((a=>(-b))=>-r) (10)--a=>b Inference Rule : Modus Ponens : a, a=>b ==> b Gentzen style proof theory (Sequent Calculus) Axiom : (1) T,φ ├ Δ,φ (2) T∪{φ} ├ Δ∪{φ} Inference Rule : // "," 在左邊表示 & // "," 在右邊表示 or // ";" 表示兩式之 & // 目的：不斷縮短算式的長度。 (&├) (├&) T, a, b ├ Δ T ├ a, Δ ; T ├ b, Δ ----------------------------- ---------------------------- T, a & b ├ Δ T ├ a & b, Δ ( or ├) (├ or ) T ├ Δ, a; T ├ Δ, b T ├ Δ, a, b ----------------------------- ---------------------------- T a or b├ Δ T ├ Δ, a or b (-├) (├ -) T ├ Δ, a T, a ├ Δ ----------------------------- ---------------------------- T, -a ├ Δ T ├ Δ, -a (=>├) (├ =>) T ├ Δ,a; T, b ├ Δ T, a ├ Δ, b ----------------------------- ---------------------------- T, a=>b ├ Δ T ├ a=>b (cut rule) T, a => Δ; T => Δ, a ------------------------- + (cut elimination theorem) = complete. T => Δ 若我們把 cut rule 用 (-├) 移位，則 cut rule 變成 T, a, -a ├ Δ Sequent : T=>Δ where T,Δ are finite sets of BE's {φ1,...φn}=>{ci1, ...cim} Informally we want to capture φ1,...,φn => ci1,...cim Davis Patumn proof method : Method : divide and conquer S ---------------------------- P = true ; P = false S[p = true] S[p=false] Case 1 : Unit clauses rule : S&{L}  S{Ltrue} Case 2 : Elimination rule : S&{Ci|L}  S Case 3 : Split rule : S  S[Ptrue] ; S[pfalse] Theorem : S is unsatisfiable iff all sets producted for Davis Patumn are unsatisfiable. φ = {(p|q) & (-q|s) & (-s|p) & (-p|r) & (-r|-p|t) }  (t & -r) -φ = (p|q) & (-q|s) & (-s|p) & (-p|r) & (-r|-p|t) & (-t | r) S ------------------------------------------------- S[p=true] ; S[p=false] {-q|s, r, -r|t, -t|r} {q, -q|s, -s, -r | -t} --------unit clause of r ----------------unit clause of -s {-q|s, t, -t} {q, -q, -r|-t} ------------- ---------------- false false If there is a P s.t P, -P in S then S is unsatisfiable. Ground Resolution Proof Theory Methodology : To prove that φ is valid, we prove that -φ is unsatisfiable instead. Inference Rule : c or x; d or -x --------------- c or d Example : s = { p or q, -p or r, -r or -s or t, q or s, -q , -r or -t} p or q -p or r \ / -r or -t q or r -r or -s or t \ / \ / q or -t q or -s or t \ / q or -s q or s \ / q -q \ / False Completeness of ground resolution theorem : φ is valid iff NIL can be deduced from S using ground resolution. Proof : Given a set of propositional variable {p1, ..., pn} A semantic tree is S T F p1 T F T F p2 P3… Each nodes represents is a partial interpretation of the variables assigned so far, where values are indicated as labeled as the edges. If S is unsatisfiable, S=c1&c2&...&cn Then each ci is a false A tree in which all pathes ends in a falsified node is called a closed semantic tree. Proposition : If S is unsatisfiable then one can get a closed semantic tree no matter how the variable are ordered. Proof of proposition Choose the (longest) path from the closed semantic tree. / / \ T F D|-P C|P Then ground resolution will produce C|D By induction , ground resolution is complete. Refinement 1 : Ordered ground resolution (assumed there is an ordering on variable, any order is good) If P is the longest atom assigning, C|P & D|-P  C|D Refinement 2 : Positive ground resolution (Choose the rightest path with all positive asignment) Refinement 3 : positive ordered ground resolution (Choose the all positive clause with longest path) The Refinement doesn't means that the produced proof will be shorter than resolution. It means that the choosing space of each step is small than the resolution case. My Refinment : Shortest first ground resolution My Refinment : Prune the other branch that is not needed any more. P|-q  prune the -p&q Boolean Ring : 設計理念： 把所有的 boolean expression 分成 class partition, 利用 normal form 來比較是否相等。 literal : . and + exclusive or 1 true 0 false Axiom : a set of rewrite rules which are used to perform reduction. . + : commutative and associative. x+y = y+x x.y = y.x (x+y)+z = x+(y+z) (x.y).z = x.(y.z) Inference Rule : x or y ==> x.y + x + y x => y ==> xy + x + 1 x = y ==> x + y + 1 -x ==> x + 1 x + 0 ==> x (identity) x . 0 ==> 0 (zero) x . 1 ==> x (unit) x . x ==> x (idempotent law) x + x ==> 0 (nilpotent law) x + y = y + x (communicative law) x . y = y . x (x+y).z ==> xz + yz (distributive law) (x + y)+ z = x + (y + z) (associative law) (x . y) . z = x . (y . z) monomial : product of distinct variables xyz, z, 1 polynomial : sum of distinct monomials xy + x + xyz = 1 Boolean ring normal form Canonical rewrite system BR (Hsiang, 1982) X | y -> xy + x + y X = y -> x + y + 1 -x -> x + 1 x => y -> xy + x + 1 x + 0 -> x x + x -> 0 x . 1 -> x x . 0 -> 0 x . x -> x x . (y+z)-> xy + xz Claim : Every Boolean expression has a unique boolean ring normal form which can be obtained through reduction. (Any Boolean formula can be uniquely translate into an equivalent BRNF.) Example : absorption law : p or (p&q) = p ppq + p + pq ==> pq + p + pq ==> p + 0 ==> p Proof : Method 1: arguing by contradiction. If BRNF is not unique then There are two BRNF (p1, p2) for some case Such that p1+p2 = m1 + m2 + … =0 Let m1 be the shortest monomial in p1+p2, Let all variable in m1 be 1, and the other variable be 0, then p1+p2 (m1 = 1) = 1, contradiction -><- Method 2: counting argument M1 + m2 + … + mk There are 2n monomial for n variable expression, So there are 2^2n BRNF for n variable expression, It can be 1-1 mapping to Boolean function. Theorem： valid 1 φ is { unsatisfiable } if its BNF is { 0 } satisfiable but not valid otherwise Remark : A BRNF is 0, 1 or m1+...+mr where each mi is a conjunction of boolean variable and the mi's are distinct from each other. Inference mechanism : reduction : given φ, reduce φ using BR until no any reduction can be done. Boolean ring equations : (x | y | -z) & (-x | -y | -z) & (y | -z | -t) if we want to satisfy the equation above then y | -z | -t = 1 De Morgan's law  -(y | -z | -t) = 0 so -y & z & t = 0 (Replace & by ., - by 1+) (1+y) . z . t = 0 (expand the equation ) zt + yzt = 0 a expression x1 | x2 | .. | xn wan be rewrite to a BRNF with 2n-1 urinal , so operator | is expensive. Simplification F = (x | y) & (x | -y) & (-x | y) & (-x | -y) Calculation : Xy + x + y + 1 = 0 0 = 0 + 0 + 1 , contradiction -><- so F is unsatisfiable. Xy + y = 0 0 + y = 0, y = 0 Xy + x = 0 0 + x = 0, x = 0 Xy = 0 let xy = 0 ↑ Simplification is sound, however, not complete. For example : Xy = 1 Yz = 1 Xz = 0 can not be simplified. Superposition (最小公倍式) Example 1 : Xy = 1 xyz = z z = 0 Yz = 1 xyz = x x = 0 Xz = 0 xyz = 0 0 = 0 Xx = x Yy = y Zz = z Example 2 : Xyz = z + 1 Xyzt = (z + 1) . t xyz = t Xyt = xy + zt Xyzt = (xy + zt) . z z = t + 1 M1 = m2  m1m1' M1' = m2' m2(m1m1'/m1) m2'(m1m1'/m1') Simplification + superposition + idempotent law  complete {x|y, -x|s, -y|t, -s|t, -t|s, -s|-t} xy = x + y + 1 xs = x yt = t st = s st = t st = 0 Davis-Putnum in Boolean ring Variety -- number of different variable in an equation. Degree -- length of the largest nominal in an equation Length -- (distinct monomials) in an equation Eample : Xyz + zy + ut + 1 variety = 5, degree = 3, length = 4 Linear : degree <= 1 X+y+z = 1, x+1 = 0, 1 = 0, … Binomial : length <= 2 Xyz + xu = 0, xy + t = 0, … Quadratic : Variety <= 2 Xy + x + y = 0, x+y+1 = 0, x+1 = 0,… Theorem Linear equation can be solved in time O(n3) (by Gaussian Elimination) Binomial equation can be solved in linear time. ( = HORN-SAT) Quadratic equations can be solved in linear time. (= 2-SAT) A reasoning model of Binomal-Linear Binomial equations B  optimize Linear equations L  optimize ↑ lift Unit equations U Important : All Boolean function can transform into the linear + binomial + unit equation by adding variable. Inference rules 1. Tautology Deletion S'{0=0} => S' S'{1=1} => S' 1 = 0 => unsatisfiable 2. Decomposition B'{x1'.x2'…xm'}  1} => B'{x1'->1, x2'->1, …,xm'->1} 3. Simplification Perform only with B or L, but not across them. 4. Unit Rule : Collect all equations x=0 or x=1 into U, Use U to simplify B, L. 5. Splitting Rule : U => U{X1} ; U{X0} 6. Transportation Given y1+y2+…+yk-1+yk = 0, where c in {0, 1} Add y1y2..yk = y1y2..yk-1 . c to B when K is odd. Add y1y2..yk = y1y2..yk-1 . (c+1) to B when K is even. Example X+y = 1 => xy = 0 X+y = 0 => xy = x X+y+z = 1 => xyz = xy, xyz = xz, xyz = yz X+y+z = 0 => xyz = 0 Discovering essential rules by local search V : the set of variables A : assignment on V For all X in V , either x = 0 in A or x = 1 in A, but not both P : partial assignment, subset of A  : Complete fence the set of partial assignments, such that given any (full) assignment A on V, P in  with P is subset of A f(x1,x2..,xm) : Schema Example : if f(x,y) = x+xy then f(x,y) = {x+xy, y+yx} fr(P) : the set of unit literals that can be inferred in (B; L; U) without the Splitting Rule. 1. Predetermine a set of schemata F. 2. Choose a complete fence  3. For each P in , evaluate fr(P) 4. W in V , with for any x in W, either x = 0 in fr(P) or x = 1 in fr(P) for all P in . 5. Bind W with f in F Find instances of f that output the same value for all p in  P1 P2 ... Pm Fr(P1) fr(P2)... fr(Pm) W ↓ F Ex : F = {x+y, xy, xy+x, x} Let F(x1, …, xm) and F'(x1', …, xm') be different formulations of the same boolean function (with xi  xi') Then F  F' can be proved Example： X1 : x+y, x1': (x|y)&(-x|-y) X2 : 1+z+t x2': (z|-t)&(-z|t) F(x1,x2) = x1+x2 F'(x1',x2') = (x1'|x2') & (-x1'|-x2') To prove (X+y) + (1+z+t)  (((x|y)&(-x|-y)) | ((z|-t)&(-z|t))) ^ (-((x|y)&(-x|-y)) | -((z|-t)&(-z|t))) Ordered binary decision diagram (OBDD) (R. E. Bryant 1986) 1. graph based NF 2. unique wrt the variable (node : CNF , DNF : no unique normal form, no variable sharing too)(BRNF : no variable sharing too) Provide an efficient way to manipulate Boolean function X Y Z F G F&g F|g F=>g 0 0 0 0 0 0 0 1 0 0 1 1 1 1 1 1 0 1 0 1 1 1 1 1 1 0 0 1 0 0 1 0 0 1 1 0 1 0 1 1 1 0 1 0 0 0 0 1 1 1 0 0 1 0 1 1 1 1 1 1 1 1 1 1 Assume an ordering on variable X1 < X2 < ... < Xn X1X2X3' + X1X2X3 X1 X1 X1 1/ \ / \ / | X2 X2 X2 X2 X2 | 1/ \ / \ => /\ /\ => / \ | X3 X3 X3 X3 1 0 0 0 1 0 / \ / \ /\ / \ 1 1 0 0 00 0 0 Idea : using Shannon entropy φ : Boolean expression φ = φ(x=1)*X + φ(x=0)*X' transform φ into its BDD give order X1<...<Xn Expansion X Share t ==> X t1==>X X<==t2 X / \ |\ /| => / \ φ(X=1) φ(X=0) |/ \| ts tu ts tu Delete Merge t1==>X t1==>t2 t1 t2 t1 t2 | | ==> | | \ / t2 t3 t3 t3 Theorem : OBDD is unique for any given φ and order. 2SAT in P A clause is definite iff it has exactly one positive literal. A clause is Horn iff it has at most one positive literal HORNSAT : HORNSAT in P (3SAT is NP complete) HORN = DEF + NEG example : (-x|-y|-z|-w|u)&(-x|-y|z)&(-z|-w|v)&(-x|-z|w) &(-x|-y)&(-x|-z|-u) & x & y We consider a truth assignment T as a set that contain all variable assigned value true. HORN-ASSIGN(φ) returns T T := empty loop Pick one unsatisfied x1&…&xn => y from Def T := T ∪ {y} until all clauses in Def are satisfied end Example : (in HORN example above) {x, y, z, w, v, u} will added into T in sequence. Claim 1 : The T produced satisfy all implication in φ Claim 2 : If there is a T’ that satisfies all implication in φ then T in T’ Proof : Let y be the first variable in T\T’ then there is a clause x1&..&xn => y s.t. x1,..,xn in T ∩ T’, so T’ !╞ (x1&..&xn=>y) -><- Claim 3 : φ is satisfiable iff T╞ φ Proof : <= trivial => by way of contradiction if T!╞φ then there is a claim -x1&..&-xn in φ s. t. T!╞-x1|..|-xn ie : {x1,..,Xn} in T If T’╞φ by claim 2 (T in T’) then T!╞{-x1,..,-xn} Every set of boolean formula can be express as a set of clauses, each of which has almost 2 positive literal. A|B|C|-D  (A|B|-T)(T|C|-D) Under HORN : classical logic and intuitionistic logic are the same. Classic Logic : law of excluded middle p|-p = true Intuitionistic logic : No law of excluded middle. Example : P(x,0,x) P(x,y,z)P(x,s(y),s(z)) // meaning : P=add Proof 1 : Exist z, P(5, 3, z) P(x,0,x) -P(x,y,z) | p(x,s(y),s(z)), -P(5,3,z) -P(5,2,z-1) -P(5,1,z-2) P(x, 0, x) bind -P(5,0,z-3) // z-3 = 5 NIL (z-2=6, z-1=7, z=8) // The resolution above is what we called input resolution Input Resolution  backward reasoning In every resolution steps, one of the clauses must be an input clause. Proof 2 : Exist z, P(5, 3, z) P(x,0,x) -P(x,y,z) | p(x,s(y),s(z)) P(x,s(0),s(x)) P(x,2,x+2) P(x, 3, x+3) bind P(5, 3, z) // x = 5, z = x+3 = 8 // The resolution above is what we called unit resolution Unit Resolution  forward reasoning In every resolution steps, one of the clauses must be a unit clauses. Theorem : In HORN logic, both unit and input resolution are complete. (Remark : not true in First Order Logic)

Sound : every theorem is a logically valid well form formula. Consistent : no well form formula V such that { |-V } and { |- not V }. Complete : every logically valid well form formula is a theorem. Incomplete Theorem : Natural Number System is consistent but incomplete, that is, there is a closed well form formula V such that neither { |- V } nor { |- not V }

Chapter 6 : Undecidability in Logic N=(Φ, π, r) Φ = { 0, s, +, *, ^ } π = { <, = } r = { <(2) , =(2) } Axiom for number theory N (Inductive definition) NT1 : x (s(x) ≠ 0) // NT1~NT3 for Natural number NT2 : x,y (s(x)=s(y) => x=y) NT3 : x (x=0 | y s(y)=x) NT4 : x (x+0 = x) // NT4~NT5 for + NT5 : x,y (x+s(y) = s(x+y)) NT6 : x (x*0 = 0) // NT6~NT6 for * NT7 : x,y (x*s(y) = x*y+x) NT8 : x (x^0 = 0) // NT8~NT9 for ^ NT9 : x,y (x^s(y) = (x^y)*x) NT10: x,y (x < s(x)) // NT10~NT13 for < NT11: x,y (x<y => s(x)≦y) NT12: x,y (-(x<y) => y≦ x) NT13: x,y,z (x<y & x<z => y<z) // NT14 for mod NT14: x,y,z,z' (mod(x,y,z) & mod(x,y,z') => z=z') NT = NT1~NT14 NT15φ : φ(0) & x (φ(x)=>φ(s(x)))=> x φ(x) // Induction Axiom (問題： NT15φ 不是 first order formula ) NT ├ ? example : NT├x,y (x+y = y+x) if we don't use the axiom NT15φ, we cannot prove this example. we can only prove that special case of this example. NT ├ 3+5 = 5+3 3+5 = s^3(0) + s^5(0) 5+3 = s^5(0) + s^3(0) = s(s^3(0) + s^4(0)) , by NT5 = s^(s^5(0) + s^2(0)) ... ... = s^5(s^3(0) + 0) = s^5(s^3(0) + 0) = s^8(0) ==by NT4= = = s^8(0) A First order sentence is ground (variable-free) if it does not contain any variable. Theorem : if φ is a ground sentence in N then N╞φ iff N├φ Bounded quantifier: x (x<5 => φ(x)) ==>  (x<5) φ(x) x (x<s(x) => φ(x)) ==>  (x<s(x)) φ(x) Bounded prenex form (b.p.f) : A sentence is in bounded prenex form if all quantifier (bounded or unbounded) precede the rest of expression. Bounded sentence : In it's b.p.f , all of it's universal quantifier is bounded. example : x<3yz<x+y φ(x,y,z) Theorem : let φ be a bounded sentence, then N╞φ iff NT├φ Proof : by induction on number of quantifiers x 不需要是 bounded, 因為我們可以一個一個試，直到找到為止 (r.e) x 一定要是 bounded, 因為若不是 bounded, 不管我們怎麼試，永遠無法確定x φ 是否成立。 Theorem : Bounded sentences = TM (Meaning : Bounded sentences are sufficient to express computation !) Without Lost of Generality (WLOG), assume TM's with 1. single tape 2. stop at "yes", "no", or does not stop. 3. never write a right(>) symbol 4. when stops, the cursor goes to the right end of the used tapes, then stop. Given TM, M=(K, Σ, δ, s) Encode symbol as numbers symbol : Σ = {0, 1, 2, ... , |Σ|-1} State : K = {|Σ|, ... , |Σ|+|K|-1 } Start : s = |Σ| right : > = 0 blank : _ = 1 "yes" = |Σ| + 1 "no" = |Σ| + 2 let b = |Σ| + |K| Configuration (snap shot) (w1, w2, ..., wm, q, u1, ... , un) is encoded as : Σ wi*b^(m+n+1-i) + q*b^n + Σ ui*b^(n-i) example : Σ = {>, _, a, b} K = { s, "yes", "no", q } 0 1 2 3 4 5 6 7 (> a a _ s b a b } 0 2 2 1 4 3 2 3 Problem : How to formulate δ into ground equation δ(a, q) = (b, p, D) s state symbol δ s q (s, a, ->) s b (s, b, ->) s _ (q, _, <-) q > (q, _, ->) ... a s _ = a _ s (2 4 1 => 2 1 4) a s a = a a s (2 4 2 => 2 2 4) a s b = a b s (2 4 3 => 2 3 4) _ s = q a (1 4 => 7 2 ) ... table(x, y) = (x=241 & y=214) | (x=242 & y=224) | ... | (x=243 & y=234)|(x=14 & y=72) | ... pads(x, x') // append _ at the end = y<b (mod(x, b, y) & y>|Σ| ) => x' = x*b+1 ( if tail(x)=y and y is a state then x' = concat(x, _) conf(x) // x is an encoding of an configuration = (y<x z<x state(x, y) & state(x, z) => z = y & nonzeros(x)) (解釋： x have only one state digit, only one >(0) in the head) ( if both x[y] & x[z] are state then y=z) nonzeros(x) = y<x u<x (mod(x, b^y, u) & (mod(x, b^(y+1), u) => x = u) (解釋: if substr(x, y, tail) = substr(x, y+1, tail) then x=substr(x, y+1, tail)) state(x, y) // yth digit is a state = z<xw<x div(x, b^y, z) & mod(z, b, w) & |Σ| ≦ w) (解釋： yStr = substr(x, y, tail); w = y[0](note: w = y[0] = x[y]); w > |Σ|) yield(x, x') // x' is the next configuration after x = pads(x, x') | y<x z1<x z2<x z2'<x z3<x z3'<x z4<x conf(x) & conf(x') & mod(x, b^y, z1) & div(x, b^y, z2) & mod(x', b^y, z1) & div(x', b^y, z2') & mod(z2, b^3, z3) & div(z2, b^3, z4) & mod(z2, b^3, z3') & div(z2', b^3, z4) & table(z3, z3') (解釋： x cursor 在最後且 x'=concat(x, _) 或 x 與 x' 都是合法的 configuration 且 且 x 依據 cursor 所在的位置分成 4 個小段 x = z1z2 & z2 = z4z3 z4 z3 [-...-][---] ---------------------- <==== x [-... ---][-...] z2 z1 z4'=z4 z3' [-...-][---] ---------------------- <==== x' [-... ---][-...] z2' z1'=z1 且 z3-->z3' 可以在 table 上查得到。) comp(x) // comp(x) formulate a computing sequence = y1<xy2<xy3<xz1<xz2<xz3<xu<xu'<x ((mod(x,b^y,z1) & mod(x,b^(y+1),z1) & div(x,b^(y+1),z2) & mod(z2,b^y2,u)&mod(z2,b^(y2+1),u)&div(z2,b^(y2+1),z3)& mod(z2,b^y2,u')& mod(z2,b^(y3+1),u') & conf(u) & conf(u')) => yield(u', u)) & (u<x mod(x,b^2,u)=>(u=b*(|Σ|+1) | u = b*(|Σ|+2))) & (u<x y<x (div(x,b^y,u) & u<b^2 & b≦ u)=> u = b*|Σ|) （解釋： the sequence of computation x0 => x1 => ... => xn where xi is configuration and xi => xi+1 is legal transformation and xn is halting state say "yes" or "no" and x0 is in start state >s>） Two language L1, L2 are recursively inseparable iff doesn't Exist recursive set R s.t. L1 ∩ R = empty and L2 in R property : If L1 and L2 are recursively inseparable and L1 ∩ L2 = empty then neither L1 nor L2 is recursive. Theroem 3.3 If L1 = {M:M(M)="yes"} and L2={M:M(M)="no"} then L1 and L2 are recursively inseparable. Proof: By way of contradiction, if Exist recursive set R s.t. R ∩ L1 = empty and L2 in R, Let MR be a TM that decides R ie: MR(x)="yes" if x in R MR(x)="no" if not x in R If MR(MR) = "yes" then MR in L1 ∩ R ≠ empty (by Def of L1) >< If MR(MR) = "no" then MR in L2 (by Def of L2) and MR not in R (by Def of MR) >< Collary 3.4 If L1' = {M:M(NULL) = "yes"} and L2' = {M:M(NULL) = "no"} then L1' and L2' are recursively inseparable. Proof : For any M, define TM M'M(x) = M(M) let R' recursively separate L1' and L2' define M"(x) = if x is an encoding of TM M', then generate M'M, if M' in R' then "yes" else "no" (ie: if M'M(x) = "no" then "yes" else "no") then R = {x: M"(x) = "yes"} is decidable Claim : R recursively separate L1 and L2 >< Proof of Claim : (1) R ∩ L1 = empty If M in R => M"(M) = "yes" => MM' in R' => not MM' in L1' => MM'(NULL) ≠ "yes" => not M in L1 >< (2) L2 in R M in L2 => M(M) = "no" => MM'(NULL) = "no" => MM' in L2' => MM' in R' => M"(M) = "yes" => M in R >< 因為theorem 3.3 已經證明了 L1, L2 是 recursive inseparable, 但若假設 R 是 recursive, 則可證出 R 會 recursive separate L1, L2, 因此、R 必然不是 recursive. ╞φ,NT├φ,N╞φ,NT╞-φ,NT├-φ,╞-φ --- ---- ---------- ----------- ---------------- ------------------ ╞φ => NT├φ by godel completeness theorem  φ (N╞φ & NT!├φ) by godel incomplete theorem None of the boundary above is recursive Theorem 6.3 |= -φ and {φ:NT├φ} are recursively inseparable. Proof : Idea : Given M, use Corollary 3.4 , find a sentence s.t. If M(NULL) = "yes" iff NT ├ φM "no" iff |= -φM By way of contradiction, If so, then there exist a recursive R s.t {φ:NT╞φ}in R and R ∩ {φ:|= -φ} = empty then define R' = {M:M in R and M is an encoding of a TM} then {M:M(NULL) = "yes"} in {M:NT├φM} in R' and {M:M(NULL) = "no" } in {M:|=-φM} ∩ R' = empty >< (because these two set are r.i) φM = NT & ψ M where ψ =  x (Comp(x) &  y<x -Comp(y) & mod(x, b^2, (|Σ|+1)*b)) (解釋： x is the least number that encode computation of M input NULL and the computation ends in "yes") Corollary 6.3.1: The following problem are undecidable Given φ (1) is φ valid ? {φ:|= φ} (ie : THEOREMHOOD is undecidable) (2) Does N |= φ ? {φ:N|=φ} (3) Does NT ├ φ ? {φ: NT ├ φ} Corollary 6.3.2: Godel incompleteness theorem (Weaker version) (1931) There is no recursively enumerable set of axiom A s.t φ A├φ iff N╞φ Proof : If such an A exist, then Th(A)={φ:A├φ} is r.e. by definition , φ N╞φ or N╞-φ then Th(N) = {φ:N╞φ} = Th(A) is r.e Th(N)' = {φ:N╞-φ} is r.e (because it's equal to Th(N)) so Th(N) is recursive >< (Because by the corollary 6.3.1, THEREMHOOD is undecidable) Remark : Godel theorem holds for the theory of (N, 0, s, +, *, <, =), But the theory of (N, 0, s, +, *, <, =) is decidable. (Presburger 1929) Equality processing : “=” assume the fllowing axioms x x=x E(x,x) x x=y  y=x -E(x,y) | E(y,x) x x=y&y=z  x=z -E(x,y) | -E(y,z) | E(x,z) For each f of arity n x1=y1&..&xn=yn  f(x1,..,xn) = f(y1,..,yn) (-E(x1,y1) |..|-E(xn,yn)|E(f(x1,..,xn),f(y1,..,yn)) For each p of arity n x1=y1&..&xn=yn&P(x1,..,xn)  P(y1,..,yn) (-E(x1,y1) |..|-E(xn,yn)|-P(x1,..,xn)|P(y1,..,yn) How to deal with “=” in theorem proving ? 1. Add an uninterpreted predicate symbol E. and add all the axioms as clauses. And then Use resolution (problem : generate to many clauses) 2. Define a new inference rule to deal with “=” Paramodulation C|s=t, D[u]  (C|D[t])x // u is a subterm of D, if sx = ux x=mgu(s,u) (Was Robinson 67) Theorem : S in FOL += is unsatisfiable iff resolution + paramodulation produce NIL from S Union { f(x1,.., xn) = f(x1,..,xn) }  function reflexible axioms (FRA) Remark : (1) Does R+P still complete without the FRA (Assume yes) (2) Paramodulation should not be done “into” a variable. (is it complete under this condition) Focus a Equational Theory Assume that “=” is the only predicates In this case, paramodulation becomes s=t; r[u] = v  r[t]x = vx (where ux=sx u is non-variable subterms of r) Example : 1. a=b; f(a)=c  f(b)=c 6. f(a)=b; g(f(x))=x  g(b)=a Rewrite method : Group theory x * x^-1 = e x * e = x (x*y)*z = x*(y*z) If we use resolution, then it may fall into infinite loop because (x*y)*z = x*(y*z) = (x*y)*z … Rewrite method : x * x^-1  e “” notion of simplification x * e  x should be a well founded ordering (x*y)*z  x*(y*z) No S1->S2->… infinite chain. Given a set of equation E={s=t} How to find a well-founded ordering > s.t E can be converted into {si->ti} where si > ti ? Let T be the set of term and > be a irreflexive, transitive relation in T, (>,T) is a simplification ordering if (1) if s > t then sx > tx (2) if s > t then u[s] > u[t] (3) if s is a proper subterm of u (u[s]) then u[s] > s Theorem : Dershowitz 82 A simplification ordering is well-founded Term rewriting theory

Arguing by contradiction theorem If Δ ∪ {-φ} is inconsistent then Δ├φ (Δ is inconsistent if Δ├φ or -φ Proof: if Δ ∪ {-φ} is inconsistent then Δ ∪ {-φ}├φ, by Decuctive Theorem, Δ ├ {-φ}=>φ, ie Δ├φ (because-φ=>φ == φ , by Hilbert style (Δ├-φ=>φ)=>φ, Δ├-φ=>φ, so Δ├φ by MP) Prenex Normal Form : Proposition : Let A and B be arbitrary first-order expressions. Then : 1. (x A & x B) = x (A&B) 2. If x does not appear free in B, (x A & B) = x (A& B) 3. If x does not appear free in B, (x A | B) = x (A| B) 4. If y does not appear in A, x A = y A[x<-y] 5. -x B = x (-B) 6. -x B = x (-B) 7. x A  B = x (AB) 8. x A  B = x (AB) An expression is said to be in prenex normal form if it consists of a sequence of quantifiers, followed by an expression that is free of quantifiers. Theorem : Any first-order expression can be transformed to an equivalent one in Prenex normal form. Skolemization (Just like Henken’s witness) Given a sentence in P.N.F. x1x2x3 A(x1,x2,x3…) --> x1x2x3 A(x1,x2,f(x1,x2),…) where f is called skolem function, is a function never appeared in the vocabulary before x1x2x3x4x5x6 P(x1,x2,x3,x4,x5,x6) --> x2x3x5 P(c,x2,x3,f(x2,x3),x5,f(x2,x3,x5)) A sentence is in clausal form if it is skolemize into x1x2x3…xn S Where S is a conjunction of clauses Property : Every sentence has a equivalent clausal form S : set of clauses = {c1,c2,.., cn} Theorem 4.1 : Given a sentence A and its equivalent set of claim S, A is inconsistent iff S is inconsistent. From now on , we don’t tgalk about sentence , only S Herbrand Universe (H = set of ground terms) Herbrand base = {p(t1,..,tn) : P is a predicate symbol and t1,t2,…,tn in H} = the set of ground atomic A ground instance of a clause C is a clause obtained from replacing its variables uniformly by terms in H. C = p(x,y) | -q(x, f(x)), | r(y) M = (H, PM) PM in Hn Example : F = {a,b, f:uniary} H = {a,b,f(a),f(b),f(f(a)), f(f(b)),...} If we have 2 uniary predicate symbols p,q A = {p(a), p(b), q(a), q(b), p(f(a)), q(f(a)), p(f(b)),…} M1:A  {T,F} M2:A  {T,F} Herbrand interpretation => A syntactic model with H as its universe (Note : this is a syntactic model, so f(a) doesn’t have to be element of U, just element of H) I1 = {p(a),q(a),-p(b),-q(b),-p(f(a)),-q(f(a)),…} Theorem : A set of clause S is unsatisfiable iff it is false in all Herbrand interpretation Let A = {A1,A2,…} be the Herbrand base of S Clause Semantic tree. A1 A2 A3 … 1 1 0 1 0 1 0 1 1 0 0 0 1 0 Herbrand Theorem : first version S is unsatisfiable iff corresponding to all semantic tree of S, there is a closed semantic tree. (Otherwise , there must be a interpretation with infinite length satisfied S) Herbrand Theorem : second version S is unsatisfiable iff there is a finite set of ground instances of S where conjunction is unsatisfiable. Ground resolution  complete ^ lift to first order logic Resolution S First order logic down to  Herbranditize lift to Unification Subsitution S(v)  T(F,V) // set of terms s.t. 1. not S(x) = x for finitely many xs 2. {x: not S(x)=x} intersect {y : not S(x)=x and y is a variable in S(x)} = empty then S is a substitution Example : S1: xf(z) S1 is a substitution ya S2: xf(x) S2 is not a substitution (because cycle, recursive sutstitute error!) ya S3: xf(y) S3 is not a substitution, xf(a) ya but may rewrite into ya S4: xf(y) S4 is not a substitution, cannot rewrite. yf(x) two expression t and s are unifiable it there is a substitution S s.t. sS=tS f(x,g(y,z),a) unified f(h(w),w,z) by assign xh(w) h(g(y,a)) S= wg(y,z)g(y,a) za f(x,g(y,z),a) cannot unified to f(h(w),w,z) If S is a substitution s.t sS = tS then S is a unifier of s and t S is a most general unifier (mgu) of S and t if (1) S is a unifier of S and t (2) For any unifier S1 of s and t, there exist a substitution S2 such that S*S2=S1 Theorem (Robinson) If s and t are unifiable then the mgu of s and t is unique upon renaming Resolution s =(S) t (see if s and are unifiable, If so return an mgu) {s1 =(S)t1,..,sn=(S)tn} 1. Decompose S union {f(s1,..,sn) =(S) f(t1,..,tn)}  S Union {s1=(S)t1, .., sn=(S)tn} 2. Clash S union {f(s1,..,sn) =(S) g(t1,..,tm)  NIL // not f=g 3. Delete S union {s=s}  S 4. Replace S Union {x=(S)t}  S[xt] union {x=(S)t} // x is not in t 5. Occurs Check S union {X=(S) Justified generalization theorem If Δ├φ, x is not free in Δ then Δ├x φ Proof: (Induction in the length of sequence of derivation, too) Consider a proof of S=(φ1,...,φn) of φ from Δ (ie : φn=φ) suppose that for all j<i, φ=>φj Δ├xφj for all j<i if φi in Λ then x φi is an axiom, too (by AX3) else if φi inΔ then φi (by hypothesis), φi=>x φi(by AX3) so x φi else // notφi in Δ∪Λ φi obtain from φj, φj=>φi by modus ponens , x φj (by induction hypothesis), x (φj=>φi) (becauseφj=>φi is an theorem in φ1..φi ∪ Δ ∪ Λ, too) x (φj=>φi)=>(( x φj)=>( x φi)) (it's a tautology) so (x φj)=>( x φi) so x φi. Rewrite theorem If φ and ψ are identical except that φ has free occurrences of x exactly at those position that ψ has free occurrence of y, then x φ=> x ψ. Proof the completeness of axiom system Δ╞φ => Δ├φ Soundness of ├ Δ├φ => Δ╞φ Proof : By induction on the length of derivation Godel's Completeness Theorem 1st form : Δ╞φ => Δ├φ 2nd form : if Δ is consistent then Δ has a model satisfy it ( Δ is consistent if it is not inconsistent) 1st form <= 2nd form Proof : if Δ╞φ (and Δ is consistent) ==> Δ∪{-φ} has no model satisfy it then by Arguing by contradiction theorem , Δ├φ. 1st form => 2nd form Proof : suppose Δhas no model , then -Δis valid but Δis consistent, so Δ!├φ&-φ Δ=>φ&-φis unsatisfiable -Δ|(φ&-φ) is unsatisfiable -Δis unsatisfiable >< (because -Δis valid) so by Arguing by contradiction theorem, Δhas a model. Proof of 2nd form Proof : Basic : given Δ over vocabulary Σ, Δ is consistent Idea : (1) Enlarge Δ to a manually consistent set Δ' (2) Build a model for Δ' M = (U, μ) is an interpretation Assume a consistent Δ (ex :{-P(a), -P(b), x P(x)} U={a,b} then expand U={a,b,c}) Idea : For each x P(x), construct a constant "witness" called Henkin constant) Step1: Add new constants c1,c2,... to Σ called the resulting alphabetΣ' Claim : Δ remain consistent over Σ' proof of claim : Suppose there is a proof (φ1,...,φn) s.t. Δ├φ&-φ that involve some constant ψ, but there are no ψ in axiom, so ├ψ in some step, replace all ψ with xi for some variable that not show up elsewhere, once again Δ├φ&-φ (after replace ψ with xi) so, Δ is inconsistent, ><. Step 2: Enlarge Δ to a consistent and complete set Δ' (note : Δ' is complete if for every expression φ, φin Δ' or -φ inΔ') Let{φ1,φ2,φ3,...}be an enumeration of all expression overΣ' Define : Δ(0) = Δ Δ(i+1) : case 1: if Δ(i-1) ∪ {φi} is consistent, and not φi = x ψ then Δ(i) = Δ(i-1) ∪ {φi} case 2: if Δ(i-1) ∪ {φi} is consistent, and φi = x ψ then (Let c be a constant not appearing in any one of the expressions φ1,...,φi-1) Δ(i)=Δ(i-1) ∪ {x ψ, ψ[x<-c]} case 3: if Δ(i-1) ∪ {φi} is inconsistent, and not φi=x ψ then Δ(i)=Δ(i-1) ∪ {-φi} case 4: if Δ(i-1) ∪ {φi} is inconsistent, and φi = x ψ then Δ(i)=Δ(i-1) ∪ {-x ψ, -ψ[x<-c]} Claim: For all i≧0, Δ(i) is consistent Proof of Claim : case 1 : Δ(i) = Δ(i-1) ∪ {φi} is consistent (by case hypothesis) case 2 : Δ(i) = Δ(i-1) ∪ {x ψ, ψ[x<-c]} is consistent, case 3 : Δ(i) = Δ(i-1) ∪ {φi} is inconsistent and Δ(i-1) is consistent , Δ(i-1)├-φi (Arguing by contradiction), so Δ(i) ∪ {-φi} is consistent case 4 : Δ(i) = Δ(i-1) ∪ {-x ψ, -ψ[x<-c]} if Δ(i) is inconsistent then Δ(i-1) ∪ {-ψ[x<-c]}├x ψ (arguing by contradiction) but Δ(i-1)├x ψ (by case hypothesis) so ><, ie : Δ(i-1) ∪ {-φ[x<-c]} is inconsistent so Δ(i-1)├{-φ[x<-c]} (arguing by contradiction) c is not show elsewhere, so we may rewrite c as variable y ie:Δ(i-1)├{-φ[x<-y]} so Δ(i-1)├y ψ[x<-y] ( justify generalization ) so Δ(i-1)├x ψ (Rewrite theorem) but Δ(i-1) ∪ {x ψ} is inconsistent (by case hypothesis)><. so Δ(i) is consistent -> Δ' is consistent Consistent : not Δ├φ&-φ // Δ(i) is consistent, so Δ' is consistent. Closed : for any x φ in Δ' there is an φ[x<-c] in Δ' Complete : for any φ, either φ in Δ' or -φ in Δ' Step 3: Build model M = (U, μ) for Δ' U = T(F')/equal = {[u]| u in T(F')} where F' is the set of function in Σ',U is the∪verse of our model M Model definition : cm = [c] fm = fm([t1],...,[tm]) = [f(t1,...,tm)] Rm = Rm([t1],...,[tm]) = [R(t1,...,tm)] , iff R in Δ' Collary : M is well defined Well defined : if ti=ti' forall 1≦i≦k then f(t1,...,tn) in Δ'=>f(t1',...,tn')inΔ' if t1=t1' for all 1≦i≦k then R(t1 ,...,tn) in Δ' => R(t1',...,tn') in Δ' proof : Δ by AX1b and AX1c Claim : M╞Δ' ( M╞φ iff φin Δ') Proof : (by induction on the structure of φ 1. if φ=R(t1,...,tk) is atomic expression then Rm([t1], ..., [tk]) iff φinΔ' 2. if φ=-ψ then M╞φ iff not M╞ψ M!╞ψ iff ψnot in Δ' (by induction hypothesis) M╞φ iff φinΔ' (because Δ'is complete, either ψ in Δ' or -ψ in Δ' ) 3. if φ=ψ1|ψ2 then M╞φ iff M╞ψ1 or M╞ψ2 M╞φ iff ψ1 in Δ' or ψ2 in Δ' M╞φ iff φin Δ' 4. if φ=ψ1&ψ2 then M╞φ iff M╞ψ1 and M╞ψ2 M╞φ iff ψ1 in Δ' and ψ2 inΔ' M╞φ iff φin Δ' 5. if φ=x ψthen Claim : φinΔ' iff ψ[x<-t] inΔ' for all term t proof of claim : => if φinΔ', x ψ=>ψ[x<-t] so Δ'├ψ[x<-t] for all t(by MP) so ψ[x<-t] inΔ' <= if φnot inΔ' then -x ψin Δ' (because Δ' is complete) ie : x -ψinΔ' by the construction of Δ' there is a c s.t -ψ[x<-c] inΔ' so not for all term t, ψ[x<-t]. Collary 1: VALIDITY is recursively enumerable Proof : trivial , because Δ' is r.e. by our building process. Collary 2: (The Compactness theorem) If all finite subset of a set of sentences Δ are satisfiable, then Δ is satisfiable. Proof : if that Δ is not satisfiable then Δ is inconsistent (because Δ is complete) so there is an derivation{φ1,...,φn}from Δ that derive ψ&-ψ ie : {φ1,...,φn} is inconsistent (unsatisfiable) >< Collary 3: (The theorem of FOPC cannot make difference of N and N') If Δ is a set of first-order sentences such that N╞Δ, then there is a model N' is a superset of N such that N'╞Δ. Proof : φi = x (x≠0&x≠1&...&x≠i) any finite subset of Δ ∪ {φi, i≧0} is consistent (because N╞Δ ∪ {φi, i<n for any n}) so Δ ∪ {φi, i≧0} is consistent. so there is a model N'╞Δ ∪ {φi, i≧0}, and N' is a superset of N (because N!╞Δ ∪ {φ, i≧0}) Collary 4: If a sentence has a model, it has a countable model. Proof : Because the model M constructed in Godel completeness proof is countable. Collary 5: (Lowenheim-Skolem Theorem) If sentence φ has finite models of arbitrary large cardinality, then it has an infinite model. Proof : Define ψ(k)= x1 ... xk (& -(xi=xj)) for all 1≦i<j≦k where k>1 φ ∪ {ψ(k): k>1} is satisfiable by compactness theorem but any model satisfied φ ∪ {ψ(k): k>1} most be infinite, so φ has an infinite model. REACHABILITY : Given G, a, b, can a reach b ? φ-graph : Given an expression φ in graph theory, given L, is L ╞ φ ? We know that φ-graph in P (chapter 1), but we have following theorem : Collary 6: There is no first-order expression φ (with two free variable x and y) such that φ-graph is the same as reachability. (ie : the power of First order logic << the power of Turing Machine) Proof : Assume that there is such an φ, then we can use φ to build the following expression φ0 = x,y φ (ie : the graph is strongly connected) φ1 = xy G(x,y) & xyz (G(x, y) & G(x, z)=>y=z) (ie : every node has exactly an edge going out) φ2 = xy G(x,y) & xyz (G(y, x) & G(z, x)=>y=z) (ie : every node has exactly an edge going in) ψ = φ0&φ1&φ2 (ie : ψ defines a cycle) since there are arbitrary large cycle, by Lowenheim-Skolem Theorem, there is an infinite cycle, it's a contradiction, so φ cannot be builded in First order expression. Boolean Logic (Zero Order Logic) : P, -P, P&Q, P|Q First Order Logic : add x P(x), x P(x), x is a term Existential Second Order Logic : add P P(x), P can be an predicate Existential Second Order Logic : Σ = (Φ, π, r) add p φ where φ is an first order expression of Σ' = (Φ, π ∪ {P}, r) M╞p φ if there is P^M in U^r(P) s.t. φ[p<-P] = true example : P (x (P(x)|P(x+1))&-(P(x)&P(x+1))) P^N = set of even number or P^N = set of odd number Law of excluded middle (P├P is always true) For a program P├P is not true, a program may going on forever. Brouwer : Intuitionistic Logic Heyking's algebra P|Q is true if there is a (constructive) proof of P or there is a proof of Q -P is true if there is a proof of P derive ╞FALSE The only difference in axiom between Heyking'a algebra and Hilbert algebra is that : Heykings : ---p=>-p Hilbert : --p=>p

PE1 : 0 exist PE2 : x' = x+1 PE3 : x' > x PE4 : If x' = y' then x = y PE5 : Principle of mathmatical Induction : If P(0) and P(x) -> P(x') then For all x, P(x)

 public static void hornReasoning(String[] rules) { TreeMap trueMap = new TreeMap(); int satisfyRuleCount; do { satisfyRuleCount = 0; for (int ri=0; ri<rules.length; ri++) { if (rules[ri].length() == 0) continue; String head = STR.head(rules[ri], "<-"); String body = STR.tail(rules[ri], "<-"); String[] conds = body.split(","); boolean isSatisfy = true; for (int ci=0; ci<conds.length; ci++) { if (conds[ci].length() == 0) continue; if (trueMap.get(conds[ci]) == null) isSatisfy = false; } if (isSatisfy) { System.out.println(rules[ri]); trueMap.put(head, "1"); rules[ri] = ""; satisfyRuleCount ++; } } } while (satisfyRuleCount > 0); }

 public static void unitResolution(String[] pRules) { Vector rules = new Vector(); for (int ri=0; ri<pRules.length; ri++) rules.add(rewrite(pRules[ri])); for (int ri=0; ri<rules.size(); ri++) { String rule1 = (String) rules.get(ri); if (rule1.indexOf(",")>0) continue; // it's not unit rule. String term = rule1; String negTerm = neg(term); for (int rj=0; rj<rules.size(); rj++) { String rule2 = (String) rules.get(rj); String exp = ","+rule2+","; if (exp.indexOf(","+negTerm+",")>0) { String unifyExp = STR.replace(exp, ","+negTerm+",", ","); String newRule = unifyExp.substring(1, unifyExp.length()-1); rules.add(newRule); System.out.println("unfiy("+rule1+"|"+rule2+")="+newRule); } } } }