Transcript MS PowerPoint format - Kansas State University

Lecture 15 of 41
More First-Order Logic Basics:
Backward Chaining, Resolution Preliminaries
Friday 24 September 2004
William H. Hsu
Department of Computing and Information Sciences, KSU
http://www.kddresearch.org
http://www.cis.ksu.edu/~bhsu
Reading:
Wikipedia entry on Ontology (CS): http://snipurl.com/9bbf
Rest of Chapter 8, 9.1-9.3, Russell and Norvig 2e
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Lecture Outline
•
Today’s Reading
– Chapter 8, Russell and Norvig
– Recommended references: Nilsson and Genesereth (excerpt of Chapter 5 online)
•
Next Week’s Reading: Chapters 9-10, R&N
•
Previously: Introduction to Propositional and First-Order Logic
– Monday (20 Sep 2004)
• First-order logic (FOL): predicates, functions, quantifiers
• Sequent rules, proof by refutation
– Wednesday (22 Sep 2004)
• Forward Chaining with Modus Ponens
• Ontology, History of Logic, Russell’s Paradox
• Unification, Logic Programming Basics
•
Today: Backward Chaining, Resolution Preliminaries, A Look Ahead
•
Next Week: Resolution, Clausal Form (CNF), Decidability of SAT
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
In-Class Discussion:
Problem Set 2
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Unification:
Definitions and Idea Sketch
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Generalized Modus Ponens
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Soundness of GMP
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Forward Chaining
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Example:
Forward Chaining
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Backward Chaining
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Example:
Backward Chaining
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Review:
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 ├

Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Completeness Redux
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Completeness in FOL
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Resolution Inference Rule
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Fun with Sentences:
Family Feud
•
Brothers are Siblings
–  x, y . Brother (x, y)  Sibling (x, y)
•
Siblings (i.e., Sibling Relationships) are Reflexive
–  x, y . Sibling (x, y)  Sibling (y, x)
•
One’s Mother is One’s Female Parent
–  x, y . Mother (x, y)  Female (x)  Parent (x, y)
•
A First Cousin Is A Child of A Parent’s Sibling
–  x, y . First-Cousin (x, y) 
 p, ps . Parent (p, x)  Sibling (p, ps)  Parent (ps, y)
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Conjunctive Normal (aka Clausal) Form [1]:
Conversion (R&N)
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Conjunctive Normal (aka Clausal) Form [2]:
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 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Skolemization
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Resolution Theorem Proving
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Example:
Resolution Proof
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Logic Programming vs. Imperative Programming
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
First-Order Satisfiability and Validity:
Undecidability and Semi-Decidability
Dual Problems
LVALID  LSAT  LSAT  LVALID (direct proof)  LVALID  LSAT (refutatio n resolution )
Decision Problem :
Given: KB, 
Decide: KB ├ ? (Is  valid?)
Procedure: Test whether KB  {¬}   , answer yes if it does
Complexity : Semi - Decidable
LH  LSAT (proof : exercise)
LH  LVALID
LVALID
LSAT
Dual Problems
LVALID
LH
LSAT
closure
under
complem.
L  L
Recursive
Languages
(REC)
LVALID  LSAT
Decision Problem (Hilbert' s Entscheidu ngsproblem ) :
Given: KB, 
Recursive Enumerable
Languages (RE)
Universe of Decision Problems
Decide: ¬(KB  )? (Is  not valid?)
Procedure: Test whether KB  {}  , answer yes if it does not
Complexity : Undecidabl e (  RE)
Ld  LSAT (proof : exercise - see Goedel' s First Incompletn ess Theorem)
Ld  LVALID
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Summary Points
•
Previously: Logical Agents and Calculi, FOL in Practice
•
Today: Resolution Theorem Proving
– Conjunctive Normal Form (clausal form)
– Inference rule
• Single-resolvent form
• General form
– Proof procedure: refutation
– Decidability properties
• FOL-SAT
• FOL-NOT-SAT (language of unsatisfiable sentences; complement of FOL-SAT)
• FOL-VALID
• FOL-NOT-VALID
•
Next Week
– More Prolog
– Implementing unification
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Terminology
•
Properties of Knowledge Bases (KBs)
– Satisfiability and validity
– Entailment and provability
•
Properties of Proof Systems
– Soundness and completeness
– Decidability, semi-decidability, undecidability
•
Normal Forms: CNF, DNF, Horn; Clauses vs. Terms
•
Resolution
•
Refutation
•
Satisfiability, Validity
•
Unification
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences