Transcript marked
Lecture 15 of 42 First-Order Logic: Resolution Discussion: AI Applications 2 of 3 Wednesday, 27 September 2007 William H. Hsu Department of Computing and Information Sciences, KSU KSOL course page: http://snipurl.com/v9v3 Course web site: http://www.kddresearch.org/Courses/Fall-2007/CIS730 Instructor home page: http://www.cis.ksu.edu/~bhsu Reading for Next Class: Section 9.5 – 9.6, p. 295 - 310, Russell & Norvig 2nd edition CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Lecture Outline Reading for Next Class: Section 9.5 – 9.6, R&N 2e Today Resolution theorem proving Prolog as related to resolution Decidability of SAT, VALID Recursive, Recursive Enumerable, and Co-RE languages MP4 & 5 preparations Friday Logic programming in real life Industrial-strength Prolog Lead-in to MP4 Next Week CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Logical Agents: Review Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Example: Backward Chaining Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Backward Chaining Question: How Does This Relate to Proof by Refutation? Answer Suppose ¬Query, For The Sake Of Contradiction (FTSOC) Attempt to prove that KB ¬Query ⊢ CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Resolution Inference Rule Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Conjunctive Normal (aka Clausal) Form: Conversion (Nilsson) and Mnemonic Implications Out Negations Out Standardize Variables Apart Existentials Out (Skolemize) Universals Made Implicit Distribute And Over Or (i.e., Disjunctions In) Operators Out Rename Variables A Memonic for Star Trek: The Next Generation Fans •Captain Picard: •I’ll Notify Spock’s Eminent Underground Dissidents On Romulus •I’ll Notify Sarek’s Eminent Underground Descendant On Romulus Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Skolemization Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Resolution Theorem Proving Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Example: Resolution Proof Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Offline Exercise: Read-and-Explain Pairs For Class Participation (PS5) With Your Assigned Partner(s) Read: Chapter 10 R&N By 13 Oct 2007 CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Logic Programming vs. Imperative Programming Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University A Look Ahead: Logic Programming as Horn Clause Resolution Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University A Look Ahead: Logic Programming (Prolog) Examples Adapted from slides by S. Russell, UC Berkeley CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Summary Points From Propositional to First-Order Proofs Generalized Modus Ponens Resolution Unification Problem Roles in Computer Science Type inference Theorem proving What do these have to do with each other? Search Patterns Forward chaining Backward chaining Fan-in, fan-out CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University Terminology From Propositional to First-Order Proofs Generalized Modus Ponens Resolution Unification Problem Most General Unifier (MGU) Roles in Computer Science Type inference Theorem proving What do these have to do with each other? Search Patterns Forward chaining Backward chaining Fan-in, fan-out CIS 530 / 730: Artificial Intelligence Wednesday. 26 Sep 2007 Computing & Information Sciences Kansas State University