Transcript MS PowerPoint format - Kansas State University

Lecture 13 of 41
More Propositional and Predicate Logic
Monday, 20 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: Propositional and First-Order Logic
– Last Wednesday (15 Sep 2004)
• Logical agent framework
• Logic in general: tools for KR, inference, problem solving
• Propositional logic: normal forms, sequent rules (modus ponens, resolution)
• First-order logic (FOL): predicates, functions, quantifiers
– Last Friday (17 Sep 2004)
• FOL agents, issues: frame, ramification, qualification problems
• Solutions: situation calculus, circumscription by successor state axioms
•
Today: FOL Knowledge Bases
•
Next Week: Resolution Theorem Proving, Logic Programming Basics
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
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
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
FOL: Complex Sentences
(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
Truth 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
Models for FOL:
Example
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Universal Quantification
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Existential Quantification
Adapted from slides by S. Russell, UC Berkeley
CIS 730: Introduction to Artificial Intelligence
Kansas State University
Department of Computing and Information Sciences
Quantifier Properties
Adapted from slides by S. Russell, UC Berkeley
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
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