Transcript MS PowerPoint format - Kansas State University

Lecture 14 of 41
First-Order Logic
and Theorem Proving
Wednesday, 22 September 2004
William H. Hsu
Department of Computing and Information Sciences, KSU
http://www.kddresearch.org
http://www.cis.ksu.edu/~bhsu
Reading:
Sections 8.1-8.3, Russell and Norvig 2e
Review: Chapter 6, R&N 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
– Last Friday (17 Sep 2004)
• FOL agents, issues: frame, ramification, qualification problems
• Solutions: situation calculus, circumscription by successor state axioms
– Monday (20 Sep 2004)
• First-order logic (FOL): predicates, functions, quantifiers
• Sequent rules, proof by refutation
•
Today: FOL Knowledge Bases and Theorem Proving
– Forward Chaining with And-Introduction, Universal Elimination, Modus Ponens
– Ontology, History of Logic, Russell’s Paradox
– Unification, Logic Programming Basics
•
Next Week: Resolution, Logic Programming, 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
Taking Stock:
FOL Inference
•
Previously: Logical Agents and Calculi
•
Review: FOL in Practice
– Agent “toy” world: 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
•
FOL Knowledge Bases
•
FOL Inference
– Proofs
– Pattern-matching: unification
– Theorem-proving as search
• Generalized Modus Ponens (GMP)
• Forward Chaining and Backward Chaining
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Automated Deduction (Chapters 8-10 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
Example Proof
•
???
•
Apply Sequent Rules to Generate New Assertions
•
Modus Ponens
And Introduction
Universal Elimination
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Search with Primitive Inference Rules
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
A Brief History of Reasoning:
Chapter 8 End Notes, 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
Knowledge Engineering
•
KE: Process of
– Choosing logical language (basis of KR)
– Building KB
– Implementing proof theory
– Inferring new facts
•
Analogy: Programming Languages / Software Engineering
– Choosing programming language (basis of software engineering)
– Writing program
– Choosing / writing compiler
– Running program
•
Example Domains
– Electronic circuits (Section 8.3 R&N)
– Exercise
• Look up, read about protocol analysis
• Find example and think about KE process for your project domain
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Ontology
•
Ontology: “What Objects Exist and Are Symbolically Representable?”
•
Issue: Grouping Objects and Describing Families
– Grouping objects and describing families
– Example: sets of sets
• Russell’s paradox: http://plato.stanford.edu/entries/russell-paradox/
• (Four) responses: types, formalism, intuitionism, Zermelo-Fraenkel set theory
– Sidebar: natural kinds (p. 232)
•
Issue: Reasoning About Time
– Modal logics (CIS 301)
– Interval logics (Section 8.4 R&N p. 238-241)
•
Example Domains
– Grocery shopping (Section 8.5 R&N); similar example in Winston 3e
– Data models for knowledge discovery in databases (KDD)
• Data dictionaries
• See grocery example, especially p. 249 - 252
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
Digression:
Decidability and Formal Languages
•
See: Hopcroft and Ullman 2e, Lewis and Papadimitriou 3e
•
Formal Languages (See: CIS 540, Other Automata Theory Course)
– Member of Turing hierarchy
• Finite state automata: regular languages
• Pushdown automata: context-free languages
• Linear bounded automata: context-sensitive languages
• Turing machines: recursive languages
– Recursive languages
•  computational model for decision problem, halts in finite number of steps
• REC: set of all recursive languages
• Example: finite searches (convert to decision problem of checking solution)
• Closed under complementation (consequence?)
– Recursive enumerable but not recursive (RE - REC)
– Not recursive ( RE)
•
What Are FOL-VALID, FOL-NOT-SAT, FOL-SAT, FOL-NOT-VALID?
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
•
Applications of Knowledge Bases (KBs) and Inference Systems
•
“Industrial Strength” KBs
– Building KBs
• Knowledge Engineering (KE) and protocol analysis
• Inductive Logic Programming (ILP) and other machine learning techniques
– Components
• Ontologies
• Fact and rule bases
– Using KBs
•
Systems of Sequent Rules: GMP/AI/UE, Resolution
•
Methodology of Inference
– Inference as search
– Forward and backward chaining
– Fan-in, fan-out
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Terminology
•
Logical Languages: WFFs, Quantification
•
Properties of Knowledge Bases (KBs)
– Satisfiability and validity
– Entailment and provability
•
Properties of Proof Systems: Soundness and Completeness
•
Knowledge Bases in Practice
– Knowledge Engineering
– Ontologies
•
Sequent Rules
– (Generalized) Modus Ponens
– And-Introduction
– Universal-Elimination
•
Methodology of Inference
– Forward and backward chaining
– Fan-in, fan-out (wax on, wax off…)
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences