Transcript CIS 730 (Introduction to Artificial Intelligence) Lecture

Lecture 12
First-Order Logic (FOL) Review
Friday, 17 September 2004
William H. Hsu
Department of Computing and Information Sciences, KSU
http://www.kddresearch.org
http://www.cis.ksu.edu/~bhsu
Reading:
Sections 7.5 – 7.10, Russell and Norvig 2e
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Lecture Outline
•
Today’s Reading
– Sections 7.5 – 7.10, Russell and Norvig 2e
– Recommended references: Nilsson and Genesereth
•
Next Week’s Reading: Chapter 8, R&N
•
Previously: Logical Agents and Calculi
– Logical agent framework
– Logic in general: tools for
• Knowledge representation
• Inference / theorem proving and problem solving / planning
– Propositional calculus
• Normal forms
• Sequent rules (modus ponens, resolution)
– Predicate logic
– First-order logic (FOL) aka first-order predicate calculus (FOPC)
•
Today: FOL Agents, Examples; Frame Problem; Situation Calculus
•
Next Week: FOL Knowledge Bases (Chapter 8, R&N)
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Review:
Simple Knowledge-Based Agent
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Chapter 7 R&N 2e
Kansas State University
Department of Computing and Information Sciences
Review: Elements of FOL
•
Logical Agents Overview (Last Tuesday)
– Knowledge Bases (KB) and KB agents
– Motivating example: Wumpus World
– Syntax of propositional calculus
– Elements of logic in general
• Syntax: What constitutes legitimate sentences aka well-formed formulae?
• Semantics: What constitutes logical entailment?
• Proof theory: What constitutes provability? Soundness? Completeness?
•
Propositional and First-Order Calculi (Last Thursday)
– Propositional calculus (concluded): inference by model checking, sequent rules
– Elements of logic in general: normal forms (CNF, DNF, Horn) and their usage
– Predicate logic without quantifiers: functions and predicates, terms and atoms
– Introduction to First-Order Logic (FOL)
• Domain theory
• Syntax of WFFs: proper scoping (existential, universal quantification)
• New features: semantics of quantification
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Validity and Satisfiability
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Proof Methods
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Inference (Sequent) Rules for
Propositional Logic
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Logical Agents:
Taking Stock
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
The Road Ahead:
Predicate Logic and FOL
•
Predicate Logic
– Enriching language
• Predicates
• Functions
– Syntax and semantics of predicate logic
•
First-Order Logic (FOL, FOPC)
– Need for quantifiers
– Relation to (unquantified) predicate logic
– Syntax and semantics of FOL
•
Fun with Sentences
•
Wumpus World 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
Syntax of FOL:
Basic Elements
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
FOL: Atomic Sentences
(Atomic Well-Formed Formulae)
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Equality
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Jigsaw Exercise [1]:
First-Order Logic Sentences
•
“Every Dog Chases Its Own Tail”
–  d . Chases (d, tail-of (d))
– Alternative Statement:  d .  t . Tail-Of (t, d)  Chases (d, t)
– Prefigures concept of Skolemization (Skolem variables / functions)
•
“Every Dog Chases Its Own (Unique) Tail”
–  d . 1 t . Tail-Of (t, d)  Chases (d, t) 
d .  t . Tail-Of (t, d)  Chases (d, t)  [ t’ Chases (d, t’)  t’ = t]
•

“Only The Wicked Flee when No One Pursueth”
–  x . Flees (x)  [¬ y Pursues (y, x)]  Wicked (x)
– Alternative :  x . [ y . Flees (x, y)]  [¬ z . Pursues (z, x)]  Wicked (x)
•
Offline Exercise: What Is An nth Cousin, m Times Removed?
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Jigsaw Exercise [2]:
First-Order Logic Sentences
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Terminology
•
Logical Frameworks
– Knowledge Bases (KB)
– Logic in general: representation languages, syntax, semantics
– Propositional logic
– First-order logic (FOL, FOPC)
– Model theory, domain theory: possible worlds semantics, entailment
•
Normal Forms
– Conjunctive Normal Form (CNF)
– Disjunctive Normal Form (DNF)
– Horn Form
•
Proof Theory and Inference Systems
– Sequent calculi: rules of proof theory
– Derivability or provability
– Properties
• Soundness (derivability implies entailment)
• Completeness (entailment implies derivability)
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
More Fun with Sentences
•
“Every Dog Chases Its Own Tail”
–  d . Chases (d, tail-of (d))
– Alternative Statement:  d .  t . Tail-Of (t, d)  Chases (d, t)
– Prefigures concept of Skolemization (Skolem variables / functions)
•
“Every Dog Chases Its Own (Unique) Tail”
–  d . 1 t . Tail-Of (t, d)  Chases (d, t) 
d .  t . Tail-Of (t, d)  Chases (d, t)  [ t’ Chases (d, t’)  t’ = t]
•

“Only The Wicked Flee when No One Pursueth”
–  x . Flees (x)  [¬ y Pursues (y, x)]  Wicked (x)
– Alternative :  x . [ y . Flees (x, y)]  [¬ z . Pursues (z, x)]  Wicked (x)
•
Offline Exercise: What Is An nth Cousin, m Times Removed?
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Wumpus World Revisited:
Interacting with FOL KBs
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Knowledge Base for
The Wumpus World
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Deducing Hidden Properties
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Keeping Track of Change:
Situation Calculus
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Describing Actions [1]:
Frame, Qualification, and Ramification Problems
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Describing Actions [2]:
Successor State Axioms
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Summary Points
•
Previously: Logical Agents and Calculi
– Logic in general: tools for KR, inference, planning
– Propositional calculus: normal forms, sequent rules
– Predicate logic
– First-order logic (FOL) aka first-order predicate calculus (FOPC)
•
Today: FOL in Practice
– FOL agents
– Example: Wumpus World in FOL
– Situation calculus
– Frame problem and variants (see R&N sidebar)
• Representational vs. inferential frame problems
• Qualification problem: “what if?”
• Ramification problem: “what else?” (side effects)
– Successor-state axioms
•
Thursday: FOL Knowledge Bases (Chapter 8, R&N), Sequent Rules for FOL
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Terminology
•
Logical Languages
– Propositional logic
– Predicates, terms, functions, atoms (atomic sentences / atomic WFFs), WFFs
– First-order logic (FOL, FOPC): universal and existential quantification
•
Properties of Knowledge Bases (KBs)
– Satisfiability and validity
– Entailment and provability
•
Properties of Proof Systems: Soundness and Completeness
•
Normal Forms: CNF, DNF, Horn; Clauses vs. Terms
•
Situation Calculus
•
Frame, Ramification, Qualification Problems
•
Successor-State Axiomatization
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences