Logic Programming & Resolution in Artificial Intelligence
Explore logic programming and resolution techniques in artificial intelligence, focusing on Prolog, backward chaining, infinite loops, redundant inference, and resolution inference rules. Dive into examples and learn how they are applied in problem-solving.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Lecture notes for Principles of Artificial Intelligence (COMS 4720/5720) Yan-Bin Jia, Iowa State University Resolution in FOL Outline I. Logic programming II. Resolution * Figures are from the textbook site.
I. Logic Programming Algorithm=Logic+Control (Robert Kowalski) Prolog (1972) is the most widely used logic programming language. Rapid prototyping Symbolic manipulation (e.g., writing compliers, parsing natural languages) A Prolog program is a set of definite clauses. // American(?) Weapon(?) Hostile(?) Sells(?,?,?) Criminal(?) criminal(X) :- american(X), weapon(Y), sells(X,Y,Z), hostile(Z). end of a clause uppercase letters for variables
Backward Chaining in Prolog Prolog recursively defines a function. Example List appending. // appending the empty list and the list Y produces the same list Y. append([], Y, Y). // [A | Z] is the result of appending [A | X] and Y provided that Z is // the result of appending X and Y. append( [A|X], Y, [A|Z]) :- append(X,Y,Z). a list whose first element is A and rest is X. Describes the relations among the three arguments of append.
Query Example (1) append([], Y, Y). (2) append( [A|X], Y, [A|Z]) :- append(X,Y,Z). Query: append(X, Y, [1, 2, 3]) append(X, Y, [1, 2, 3]) (1) (2): A = 1 append(X1, Y, [2,3]) (1) append([], Y, Y) X = [] Y = [1,2,3] (2): A = 2 append(X2, Y, [3]) append([], Y, Y) X1 = [] X = [1 | X1] = [1] Y = [2,3] (2): A = 3 (1) append(X3, Y, []) (1) X = [1 | [2 | [] ]] = [1, 2] Y = [3] X = [1 | [2 | [3 | [] ]]] = [1, 2, 3] Y = []
Infinite Loop Finds if a path exists between two nodes in a directed graph. switch order path(X,Z) :- link(X, Z). path(X,Z) :- path(X,Y), link(Y,Z). path(X,Z) :- path(X,Y), link(Y,Z). path(X,Z) :- link(X, Z). Querypath(a, c) link(A, B) link(B, C) Infinite loop!
Redundant Inference path(X,Z) :- link(X, Z). path(X,Z) :- path(X,Y), link(Y,Z). Querypath(A1, J4) Prolog performs 877 inferences (most of which involve nodes from which the goal is unreachable). Forward chaining performs only 62 inferences.
II. Resolution Inference Rule ?1 ?? ??, ?1 ?? ?? SUBST(?, ?1 ?? 1 ??+1 ?? ?1 ?? 1 ??+1 ??) where ? = UNIFY ??, ?? makes ?? and ?? two complementary literals. ( ) Animal(?(?)) Loves(?(?), ?) ( Loves(?, ?) Kills(?, ?)) unifier: ? = {?/?(?), ?/?} resolvent: Animal(?(?)) Kills(?(?), ?)) Binary resolution as given above does not yield a complete inference procedure. Full resolution does. It resolves subsets of literals in each clause that are unifiable.
Example Proof 1 The crime example: American(?) Weapon(?) Sells(?, ?, ?) Hostile(?) Criminal(?) Missile(?) Owns(Nono,?) Sells(West,?,Nono) Missile(?) Weapon(?) Enemy(?, America) Hostile(?) Owns(Nono,?1) Missile(?1) American(West) Enemy(Nono,America) We prove Criminal(West) by adding Criminal(West) and deriving the empty clause .
Resolution Proof 1 {?/West} {?/y} {?/?1 } {?/?1, ?/Nono} {?/Nono} Like backward chaining on the main spine. Always resolve with a clause containing a positive literal that unifies with the leftmost literal of the current clause on the spine.
Example Proof 2 (with Skolemization) Everyone who loves all animals is loved by someone. Anyone who kills an animal is loved by no one. Jack loves all animals. Either Jack or Curiosity killed the cat, who is named Tuna. Did Curiosity kill the cat? A. ? ? Animal ? Loves ?,? ? Loves(?,?) B. ? ? Animal ? Kills ?,? ( ? Loves(?,?)) C. ? Animal(?) Loves(Jack,?) D. Kills(Jack,Tuna) Kills(Curiosity,Tuna) E. Cat(Tuna) Background knowledge F. ? Cat(?) Animal(?) Negated goal Kills(Curiosity,Tuna) G.
Converting to CNF ? ( ? Animal ? Loves ?, ? ) ( ? Loves(?,?)) A. ?(?) ?(?) Animal ?(?) Loves(?(?),?)) A1. A2. Loves ?,?(?) Loves(?(?),?)) B. Animal ? Kills ?,? Loves(?,?)) Animal ? Loves(Jack,?)) C. Kills Jack,Tuna Kills Curiosity, Tuna D. E. Cat Tuna Cat ? Animal(?) F . G. Kills Curiosity, Tuna
Resolution Proof 2 Rename ? as ?1 Rename ? as ?2 Loves ?2, ?(?2) Loves(Jack, ? )) 1 ? = {?1/?(Jack), ?2/Jack} Paraphrased in English: Suppose Curiosity did not kill Tuna. We know that either Jack or Curiosity did; thus Jack must have. Now, Tuna is a cat and cats are animals, so Tuna is an animal. Because anyone who kills an animal is loved by no one, we know that no one loves Jack. On the other hand, Jack loves all animals, so someone loves him; so we have a contradiction. Therefore, Curiosity killed the cat.
Completeness of Resolution Theorem If a set ? of sentences is unsatisfiable, then resolution will always be able to derive a contradiction. Not all logical consequences of ? can be generated using resolution. A sentence entailed by ? can always be established using resolution. We can use resolution to find all answers to a question ?(?)by proving that KB ? ? is unsatisfiable.
