Ve492: Introduction to Artificial Intelligence
PL Agents & First Order Logic
Paul M-SJTU Joint Institute Slides adapted from AIMA, UM, CMU
Copyright By PowCoder代写 加微信 powcoder
Learning Objectives
❖ How to implement a logical agent with PL?
❖ What are the limitations of propositional logic?
❖ What is first-order logic?
❖ How to perform inference in first-order logic?
❖ Implementing a logical agent using propositional logic
❖ First-order logic
Recap: Logical Agent
❖ Collec&on of sentences represen&ng facts and rules we know about the world Sentence
❖ Logical statement
❖ Composi&on of logic symbols and operators
Model (vs World)
❖ Complete assignment of symbols to True/False
❖ Sentence we want to know if it is provably True, provably False, or unsure.
World vs Model
❖ A world is a state where the agent can be in
❖ A model is an abstraction of a world ❖ e.g., if only P1,2 P2,2 P3,1, (F, F, T) or (T, F, F)
Recap: Logical Agent
❖ Input: model, sentence
❖ Does model satisfy sentence?
❖ Is this sentence true in this model? ❖ PL-TRUE
Entailment
❖ Input: sentence1, sentence2
❖ If I know sentence1 holds, then do I know sentence2 holds?
❖ Each model that satisfies sentence1 must also satisfy sentence2 ❖ How to compute entailment?
❖ Model checking, e.g., TT-ENTAILS ❖ Theorem proving
Recap: Logical Agent
❖ Input: sentence
❖ Is sentence true in all possible models?
Satisfiable
❖ Input: sentence
❖ Can find at least one model that satisfies this sentence?
(We often want to know what that model is) ❖ Is it possible to make sentence true?
❖ DPLL (efficient SAT solver)
Vocabulary: Propositional Logic
❖ Atomic sentence: True, False, Symbol, ¬Symbol Clause
❖ of literals: 𝐴 ∨ 𝐵 ∨ ¬𝐶 Conjunc/ve Normal Form (CNF)
❖ of clauses: (𝐴 ∨ 𝐵 ∨ ¬𝐶) ∧ (¬𝐴 ∨ 𝐶¬𝐷) Definite clause
❖ of literals, exactly one is ❖ ¬𝐴∨𝐵∨¬𝐶
Horn clause
❖ of literals, at most one is ❖ All definite clauses are Horn clauses
Implementing a Logical Agent
❖ Select symbols to describe problem
❖ 𝑃!,#, 𝑊!,#, G!,#, 𝐵!,#, S!,$, …
❖ TELL initial knowledge of agent
❖ Initial state: ¬𝑃%,% , ¬𝑊%,%
❖ “Physics” of the world: ⋁&,$ 𝑊&,$ , ¬(𝑊&,$ ∧ 𝑊&!,$! )…
❖ Encode all these facts in PL; not easy!
❖ How to make decisions?
❖ Fully-based on PL
PL-based Example
❖ Initial knowledge requires transition model
❖ How to encode the agent’s location? Is it sufficient to add 𝐿!,# for all i and j?
❖ Weneed𝐿&,$ foralli,j,t!
❖ Symbols that depend on time are called fluents
❖ We need symbols for actions:
❖ 𝐹𝑜𝑟𝑤𝑎𝑟𝑑’, 𝑇𝑢𝑟𝑛𝐿𝑒𝑓𝑡’,…
❖ Transition model (successor-state axioms) expressed for all t:
❖ 𝐹'(% ⟺ (𝐹’ ⋀ ¬𝐴𝑐𝑡𝑖𝑜𝑛𝐶𝑎𝑢𝑠𝑒𝑠𝑁𝑜𝑡𝐹’) ∨ 𝐴𝑐𝑡𝑖𝑜𝑛𝐶𝑎𝑢𝑠𝑒𝑠𝐹’
#$! ‘ ‘ ‘(%
❖ E.g., 𝐿!,! ⟺ (𝐿%,% ∧ ¬𝐹𝑜𝑟𝑤𝑎𝑟𝑑 ∨ 𝐵𝑢𝑚𝑝
”’ (𝐿%,) ∧ 𝑆𝑜𝑢𝑡h ∧ 𝐹𝑜𝑟𝑤𝑎𝑟𝑑
”’ (𝐿),% ∧ 𝑊𝑒𝑠𝑡 ∧ 𝐹𝑜𝑟𝑤𝑎𝑟𝑑
PL-based Example
❖ Construct a sentence that includes
❖ Initial state, domain knowledge
❖ Transition model for all 𝑡 = 1,…,𝑇
❖ Axioms about the world (e.g., preconditions and action exclusion)
❖ Goal state: HaveGold* ∧ ClimbOut*
❖ Give the sentence to SAT solver
❖ If not satisfiable increment 𝑇, and repeat
❖ Extract plan by choosing action at timestep t if corresponding fluent is true
❖ Limitation: only works with fully observable problem
Hybrid Example: Wumpus World
First Order Logic
USE FIRST-ORDER LOGIC
Pros and Cons of Propositional Logic
❖ Propositional logic is declarative: pieces of syntax correspond to facts
❖ Propositional logic allows partial/disjunctive/negated information
(unlike most data structures and databases)
❖ Propositional logic is compositional:
e.g., meaning of 𝐵W,W ∧ 𝑃!,# is derived from meaning of 𝐵W,W and of 𝑃!,#
❖ Meaning in propositional logic is context-independent
(unlike natural language, where meaning depends on context)
❖ Propositional logic has very limited expressive power (unlike natural language)
e.g., cannot say “pits cause breezes in adjacent squares” except by writing one sentence for each square
Pros and Cons of Propositional Logic
❖ Rules of Chess:
❖ 100,000 pages in propositional logic
❖ 1 page in first-order logic
❖ Rules of Wumpus World:
❖ ∀𝑥, 𝑦 Breezy([𝑥, 𝑦]) ⇔ ∃𝑎, 𝑏 Adjacent([𝑎, 𝑏], [𝑥, 𝑦]) ∧ Pit([𝑎, 𝑏])
∀𝑥, 𝑦, 𝑎, 𝑏 Adjacent([𝑥, 𝑦], [𝑎, 𝑏]) ⇔
[𝑎, 𝑏] ∈ {[𝑥 + 1, 𝑦], [𝑥 − 1, 𝑦], [𝑥, 𝑦 + 1], [𝑥, 𝑦 − 1]}
First-Order Logic
❖ Whereas propositional logic assumes world contains facts, first-order logic assumes the world contains:
Objects: people, integers, body parts, JI courses, events, dates…
Constants: , 127, Ve492, French revolution Relations: knows, is prime, is US president,
prerequisite, occurred after, …
Functions: best friend forever (BFF), successor, left leg of, end of, …
❖ These define possible worlds
Syntax and Semantics: Terms
❖ A term refers to an object; it can be: ❖ a constant symbol, e.g., A , B, EvilKingJohn
❖ The possible world fixes these referents ❖ a function symbol with terms as arguments,
e.g., BFF(EvilKingJohn)
❖ The possible world specifies the value of the
function, given the referents of the terms
❖ BFF(EvilKingJohn) -> BFF(2) -> 3 ❖ a variable, e.g., x
Syntax and Semantics: Atomic Sentences
❖ An atomic sentence is an elementary proposition (cf symbols in PL)
❖ A predicate symbol with terms as arguments, e.g., Knows(A,BFF(B))
❖ True iff the objects referred to by the terms are in the relation referred to by the predicate
❖ Knows(A,BFF(B)) -> Knows(1,BFF(2)) -> Knows(1,3) -> F
❖ An equality between terms, e.g., BFF(BFF(BFF(B)))=B
❖ True iff the terms refer to the same objects
❖ BFF(BFF(BFF(B)))=B -> BFF(BFF(BFF(2)))=2 -> BFF(BFF(3))=2 -> BFF(1)=2 -> 2=2 -> T
Syntax and Semantics: Complex Sentences
❖ Sentences with logical connectives ❖ ¬𝛼,𝛼∧𝛽,𝛼∨𝛽,𝛼⇒𝛽,𝛼⇔𝛽
❖ Sentences with universal or existential quantifiers, e.g.,
❖ ∀x Knows(x, BFF(x))
❖ True in world w iff true in all extensions of w where x
refers to an object in w
❖ x -> 1: Knows(1,BFF(1)) -> Knows(1,2) -> T
❖ x -> 2: Knows(2,BFF(2)) -> Knows(2,3) -> T
❖ x -> 3: Knows(3,BFF(3)) -> Knows(3,1) -> F
Syntax and Semantics: Complex Sentences
❖ Sentences with logical connectives ❖ ¬𝛼,𝛼∧𝛽,𝛼∨𝛽,𝛼⇒𝛽,𝛼⇔𝛽
❖ Sentences with universal or existential quantifiers, e.g.,
❖ ∃x Knows(x, BFF(x))
❖ True in world w iff true in some extension of w where x
refers to an object in w
❖ x -> 1: Knows(1,BFF(1)) -> Knows(1,2) -> T
❖ x -> 2: Knows(2,BFF(2)) -> Knows(2,3) -> T
❖ x -> 3: Knows(3,BFF(3)) -> Knows(3,1) -> F
Syntax of First Order Logic
❖ Sentence → AtomicSentence | ComplexSentence ❖ AtomicSentence → Predicate | Predicate(Term, …)
| Term = Term
❖ Term → Function(Term, …) | Constant | Variable
❖ ComplexSentence → (Sentence) | ¬ Sentence | Sentence ∧ Sentence
| Sentence ∨ Sentence
| Sentence ⇒ Sentence
| Sentence ⇔ Sentence
| Quantifier variable,… Sentence
❖ Quantifier→∀|∃
❖ Constant→A|X_1|John|…
❖ Variable→a|x|s|…
❖ Predicate → True | False | Even | Raining | NeighborOf | Loves |… ❖ Function → Successor | Temperature | Mother | LeftLeg | …
Spectrum of Representations
Search, game-playing MDP, RL
CSPs, planning, propositional logic, Bayes nets, neural nets, RL with function approx.
First-order logic, databases, probabilistic programs
Application in Autonomous Driving
❖ Autonomous driving
❖ Mission planner
❖ Behavioral systems: e.g., lane driving, intersection handling
❖ Motion planner
❖ Neuro-symbolic approach for tactical decision-making
Example: Let’s Have Fun with FOL!
❖ Translate
❖ Everybody loves somebody
❖ Everybody’s looking for something
❖ Some of them want to use you
❖ Some of them want to get used by you
❖ All greedy kings are evil
❖ Some greedy kings are evil
Example: Let’s Formalize Natural Numbers
❖ Objects = 𝕆
❖ Constant: 0
❖ Function:S∶ 𝕆→𝕆
❖ Predicates: NatNum : 𝕆 → 𝔹 ❖ NatNum(0)
❖ ∀𝑛 NatNum(𝑛) ⇒ NatNum(S(𝑛))
❖ Addition: + : 𝕆×𝕆 → 𝕆
❖ ∀𝑛 NatNum(𝑛) ⇒ +(𝑛, 0) = 𝑛
❖ ∀𝑛, 𝑚 NatNum(𝑛) ∧ NatNum(𝑚) ⇒ +(𝑛, S(𝑚)) = S(+(𝑛, 𝑚))
Semantics of FOL
❖ Given a set of objects, a model is defined by an interpretation:
❖ Which object each constant refers to?
❖ How to define each relation?
❖ How to define each function?
❖ Model and interpretation => evaluation of FOL sentences
❖ Logical consequences still via entailment (discussed later)
Example: Let’s Formalize Natural Numbers
❖ Objects = N
❖ Constant: 0
❖ Function:S:N→N
❖ Predicates: NatNum : N → 𝔹 ❖ NatNum(0)
❖ ∀𝑛 NatNum(𝑛) ⇒ NatNum(S(𝑛))
❖ Addition: + : N×N → N
❖ ∀𝑛 NatNum(𝑛) ⇒ +(𝑛, 0) = 𝑛
❖ ∀𝑛, 𝑚 NatNum(𝑛) ∧ NatNum(𝑚) ⇒ +(𝑛, S(𝑚)) = S(+(𝑛, 𝑚))
Quiz: FOL on N
❖ Choose the correct FOL sentence for “Any square number is
not a prime.”
1. ∃𝑛∃𝑚 𝑛 = 𝑚×𝑚 ⇒ ¬Prime(𝑛)
2. ∀𝑛∃𝑚 𝑛 = 𝑚×𝑚 ⇒ ¬Prime(𝑛)
3. ∃𝑛∃𝑚 (𝑛 = 𝑚×𝑚) ∧ (¬Prime(𝑛)) 4. ∀𝑛∃𝑚 (𝑛 = 𝑚×𝑚) ∧ (¬Prime(𝑛))
Tarski’s World
❖ Book + software
❖ Open source version
Let’s Formalize Wumpus World
❖ Objects:
❖ Right, Left, Forward, Shoot, Grab, Release, Climb ❖ Nforlocationandtime
❖ Functions:
❖ Turn(Right) ❖…
❖ Predicates:
❖ Breezy([𝑥, 𝑦]), Pit([𝑎, 𝑏]), Adjacent([𝑎, 𝑏], [𝑥, 𝑦]), At([𝑥, 𝑦], 𝑡), Action(𝑎, 𝑡)
❖ West(𝑡), East(𝑡), North(𝑡), South(𝑡) ❖…
Let’s Formalize Wumpus World
❖ Physics of the world:
∀𝑥, 𝑦, 𝑎, 𝑏 Adjacent([𝑥, 𝑦], [𝑎, 𝑏]) ⇔
[𝑎, 𝑏] ∈ {[𝑥 + 1, 𝑦], [𝑥 − 1, 𝑦], [𝑥, 𝑦 + 1], [𝑥, 𝑦 − 1]}
❖ ∀𝑥, 𝑦 Breezy 𝑥, 𝑦 ⇔ ∃𝑎, 𝑏 Adjacent([𝑎, 𝑏], [𝑥, 𝑦]) ∧ Pit([𝑎, 𝑏])
❖ ∀𝑥, 𝑦, 𝑡 At([𝑥, 𝑦], 𝑡) ∧ Breeze(𝑡) ⇒ Breezy([𝑥, 𝑦])
∀𝑥, 𝑦, 𝑡 At([𝑥, 𝑦], 𝑡) ⇔
(At([𝑥 + 1, 𝑦], 𝑡 − 1) ∧ West(𝑡 − 1) ∧ Action(𝐹𝑜𝑟𝑤𝑎𝑟𝑑, 𝑡 − 1)) ∨ (At([𝑥 − 1, 𝑦], 𝑡 − 1) ∧ East(𝑡 − 1) ∧ Action(𝐹𝑜𝑟𝑤𝑎𝑟𝑑, 𝑡 − 1)) ∨ (At([𝑥, 𝑦 − 1], 𝑡 − 1) ∧ North(𝑡 − 1) ∧ Action(𝐹𝑜𝑟𝑤𝑎𝑟𝑑, 𝑡 − 1)) ∨ (At([𝑥, 𝑦 + 1], 𝑡 − 1) ∧ South(𝑡 − 1) ∧ Action(𝐹𝑜𝑟𝑤𝑎𝑟𝑑, 𝑡 − 1)) ∨ (At([𝑥, 𝑦], 𝑡 − 1) ∧ (∃𝑎 ¬(𝑎 = 𝐹𝑜𝑟𝑤𝑎𝑟𝑑) ∧ Action(𝑎, 𝑡 − 1))) ∨ (At([𝑥, 𝑦], 𝑡 − 1) ∧. . .
Inference Algorithms
Propositionalization Lifted Inference
Inference in FOL
❖ Entailment is defined exactly as for PL:
❖ 𝛼⊨𝛽iffineverymodelwhere𝛼istrue,𝛽isalsotrue
❖ E.g., ∀x Knows(x,Obama) entails ∃y∀x Knows(x,y)
❖ Given an existentially quantified query, a positive answer also provides a
suitable substitution (or binding) for the variable(s):
❖ KB = ∀x Knows(x,Obama)
❖ Query = ∃y∀x Knows(x,y)
❖ Answer = Yes, {y/Obama}
❖ Applying the substitution should produce a sentence that is entailed by KB
Inference in FOL: Propositionalization
❖ Convert (KB ∧ ¬𝛼) to PL, use a PL SAT solver to check (un)satisfiability
❖ Trick: replace variables with ground terms, convert atomic sentences to symbols
❖ ∀x Knows(x,Obama) and Democrat(Hillary_Clinton)
❖ Knows(Obama,Obama) and Knows(Hillary_Clinton,Obama) and
Democrat(Hillary_Clinton)
❖ K_O_O ∧ K_C_O ∧ D_C
❖ and ∀x Knows(Mother(x),x)
❖ Knows(Mother(Obama),Obama), Knows(Mother(Mother(Obama)),Mother(Obama)), …
❖ Real trick: for k = 1 to infinity, use terms of function nesting depth k
❖ If entailed, will find a contradiction for some finite k; if not, may continue for ever; semidecidable
Inference in FOL: Lifted Inference
❖ Apply inference rules directly to first-order sentences, e.g.,
❖ KB = Person(Socrates), “x Person(x) Þ Mortal(x)
❖ conclude Mortal(Socrates)
❖ The general rule is a version of :
❖ Given a[x] Þ b[x] and a’, where a’s = a[x]s for some substitution s conclude b[x] s ❖ s is {x/Socrates}
❖ Given Knows(x,Obama) and Knows(y,z) Þ Likes(y,z) ❖ s is {y/x, z/Obama}, conclude Likes(x,Obama)
❖ Examples: Prolog (backward chaining), Datalog (forward chaining), production rule systems (forward chaining), resolution theorem provers
Gödel’s Incompleteness Theorem
❖ For any logic and consistent KB beyond very simple, some true statements are unprovable.
❖ “beyond very simple” means “capable of expressing the theory of numbers”, which requires the mathematical induction schema.
❖ Gödel showed how to express the statement, “This sentence is not provable.”
– The two difficult parts are to express, in logic:
❖ “This sentence S” (self-referentiality) ❖ provable(S)
– The paradox of the sentence proves the theorem.
Concluding Remarks
❖ FOL is a very expressive formal language
❖ Many domains of common-sense and technical knowledge can be written in FOL (e.g., circuits, software, planning, law, network and security protocols, product descriptions, e-commerce transactions, geographical information systems, Google Knowledge Graph, Semantic Web).
❖ Inference is semidecidable in general; many problems are efficiently solvable in practice
❖ Inference technology for logic programming is especially efficient.
❖ For more information:
❖ AIMA, Chapter 8 for First-Order Logic
❖ AIMA, Chapter 9 for Inference in First-Order Logic
❖ AIMA, Chapter 12 for Knowledge Representation
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com