1Foundations of Artificial IntelligenceFirst-Order LogicCS472 – Fall 2007Thorsten JoachimsFirst-Order Logic• Idea:– Don’t treat propositions as “atomic” entities.• First-Order Logic:– Objects: cs472, fred, ph219, emptylist …– Relations/Predicates: is_Man(fred), Located(cs472, ph219) …• Note: Relations typically correspond to verbs– Functions: Pair(search,Pair(learning,Pair(kbsystems, emptylist)))– Connectives: ∧, ∨ , ¬, ⇒, ⇔– Quantifiers: •Universal: ∀ x: ( is_Man(x) ⇒ is_Mortal(x) )•Existential: ∃ y: ( is_Father(y, fred) ) Example: Representing Facts in First-Order Logic1. Lucy* is a professor2. All professors are people.3. Fuchs is the dean.4. Deans are professors.5. All professors consider the dean a friend or don’t know him.6. Everyone is a friend of someone.7. People only criticize people that are not their friends. 8. Lucy criticized Fuchs. * Name changed for privacy reasons.Example: ProofKnowledge base:•is-prof(lucy)• ∀ x ( is-prof(x) → is-person(x) )• is-dean(fuchs)• ∀ x (is-dean(x) Æ is-prof(x))• ∀ x (∀ y ( is-prof(x) ∧ is-dean(y) → is-friend-of(y,x) ∨ ¬ knows(x, y) ) )• ∀ x (∃ y ( is-friend-of (y, x) ) )• ∀ x (Vy (is-person(x) ∧ is-person(y) ∧ criticize (x,y) → ¬ is-friend-of (y,x)))• criticize(lucy,fuchs)Question: Is Fuchs no friend of Lucy?¬ is-friend-of(fuchs,lucy)Knowledge Engineering1. Identify the task. 2. Assemble the relevant knowledge.3. Decide on a vocabulary of predicates, functions, and constants. 4. Encode general knowledge about the domain.5. Encode a description of the specific problem instance. 6. Pose queries to the inference procedure and get answers. 7. Debug the knowledge base. Inference Procedures: Theoretical Results• There exist complete and sound proof procedures for propositional and FOL. – Propositional logic• Use the definition of entailment directly. Proof procedure is exponential in n, the number of symbols. • In practice, can be much faster…• Polynomial-time inference procedure exists when KB is expressed as Horn clauses: where the Piand Q are non-negated atoms. – First-Order logic• Godel’s completeness theorem showed that a proof procedure exists…• But none was demonstrated until Robinson’s 1965 resolution algorithm. • Entailment in first-order logic is semidecidable.2Resolution Rule of InferenceGeneral Rule:Example:Note: Eijcan be negated.Algorithm: Resolution Proof• Negate the theorem to be proved, and add the result to the knowledge base. • Bring knowledge base into conjunctive normal form (CNF) – CNF: conjunctions of disjunctions– Each disjunction is called a clause.• Until there is no resolvable pair of clauses,– Find resolvable clauses and resolve them.– Add the results of resolution to the knowledge base.– If NIL (empty clause) is produced, stop and report that the (original) theorem is true.• Report that the (original) theorem is false. Resolution Example: Propositional Logic• To prove: ¬ P• Transform Knowledge Base into CNF• Proof1. ¬ P ∨ Q Sentence 12. ¬ Q ∨ R Sentence 23. ¬ R Sentence 34. P Assume opposite5. Q Resolve 4 and 16. R Resolve 5 and 27. nil Resolve 6 with 3Resolution Example: FOLExample: Prove bird (tweety)Axioms: Regular CNF1:2:3:4:Resolution Proof1. Resolve 3 and 1, specializing (i.e. “unifying”) tweety for x. Add ¬feathers(tweety)2. Resolve 4 and 2. Add NIL.Resolution Theorem ProvingProperties of Resolution Theorem Proving:– sound (for propositional and FOL)– (refutation) complete (for propositional and FOL)Procedure may seem cumbersome but note that can be easily automated. Just “smash” clauses until empty clause or no more new clauses. UnificationUnify procedure: Unify(P,Q) takes two atomic (i.e. single predicates) sentences P and Q and returns a substitution that makes P and Q identical. Rules for substitutions: – Can replace a variable by a constant.– Can replace a variable by a variable.– Can replace a variable by a function expression, as long as the function expression does not contain the variable.Unifier: a substitution that makes two clauses resolvable.3Unification - PurposeGiven: ¬ Knows (John, x) ∨ Hates (John, x)Knows (John, Jim)Derive:Hates (John, Jim)Unification:Need unifier {x/Jim} for resolution to work.Add to knowledge base:Unification (example)Who does John hate? ∃x: Hates (John, x) Knowledge base (in clause form): 1. ¬ Knows (John, v) ∨ Hates (John, v)2. Knows (John, Jim)3. Knows (y, Leo)4. Knows (z, Mother(z))5. ¬ Hates (John, x) (since ¬∃x: Hates (John, x) Ù∀ x: ¬Hates(John,x))Resolution with 5 and 1:unify(Hates(John, x), Hates(John, v)) = {x/v}6. ¬ Knows (John, v) Resolution with 6 and 2: unify(Knows(John, v), Knows(John, Jim))= {v/Jim}or resolution with 6 and 3: unify(Knows (John, v), Knows (y, Leo)) = {y/John, v/Leo}or Resolution with 6 and 4: unify(Knows (John, v), Knows (z, Mother(z))) = {z/John, v/Mother(z)}Answers:1. Hates(John,x) with {x/v, v/Jim} (i.e. John hates Jim)2. Hates(John,x) with {x/v, y/John, v/Leo} (i.e. John hates Leo)3. Hates(John,x) with {x/v, v/Mother(z), z/John} (i.e. John hates his mother)Most General UnifierIn cases where there is more than one substitution choose the one that makes the least commitment (most general) about the bindings. UNIFY (Knows (John,x), Knows (y,z))= {y / John, x / z}not {y / John, x / z, z / Freda}not {y / John, x / John, z / John}…See R&N for general unification algorithm. O(n2) with RefutationConverting More Complicated Sentences to CNF1. Eliminate ImplicationsSubstitute ¬ E1 ∨ E2for E1→ E22. Move negations down to the atomic formulasEquivalence Transformations:Result:43. Eliminate Existential Quantifiers: SkolemizationHarder cases:There is one argument for each universally quantified variable whose scope contains the Skolem function.Easy case: 4. Rename variables as necessaryWe want no two variables of the same name.5. Move the universal quantifiers to the leftThis works because each quantifier uses a unique variable name.6. Move disjunctions down to the literals7. Eliminate the conjunctions8. Rename all variables, as necessary, so no two have the same name59. Eliminate the universal quantifiersAlgorithm: Putting Axioms into Clausal Form1. Eliminate the implications.2. Move the negations down to the atomic formulas.3. Eliminate the existential quantifiers. 4. Rename the variables, if necessary.5. Move the universal