Propositional Logic 10S3001 PDF

Propositional Logic 10S3001 – Artificial Intelligence Samuel I. G. Situmeang Faculty of Informatics and Electrical Engineering 1  Objectives Students are able: ▪ to explain the concept of knowledge-based agents cle...

Propositional Logic 10S3001 – Artificial Intelligence Samuel I. G. Situmeang Faculty of Informatics and Electrical Engineering 1  Objectives Students are able: ▪ to explain the concept of knowledge-based agents clearly. ▪ to explain the concept of logical agents clearly. ▪ to represent information from the environment in the form of logical propositions. ▪ to apply inference to propositional logic by using propositional logic inference rules. 10S3001-AI | Institut Teknologi Del 2 Siswa mampu: untuk menjabarkan konsep knowledge-based agent dengan jelas. untuk menjabarkan konsep logical agent dengan jelas. untuk merepresentasi informasi dari lingkungan dalam bentuk logika proposisi. untuk menerapkan inferensi pada logika proposisi dengan menggunakan aturan inferensi logika proposisi. 2 Overview ▪ Knowledge-based Agents ▪ The Wumpus World ▪ Logical Agent ▪ Building Propositions ▪ Inference Rules ▪ Model Checking and Inference ▪ Theorem Proving and Proof by Resolution ▪ Conversion to CNF and Resolution Algorithm ▪ Forward and Backward Chaining 10S3001-AI | Institut Teknologi Del 3 3  Knowledge-based Agents 10S3001-AI | Institut Teknologi Del 4 4 Knowledge-based Agents “Logical AI: The idea is that an agent can represent knowledge of its world, its goals and the current situation by sentences in logic and decide what to do by inferring that a certain action or course of action is appropriate to achieve its goals.“ John McCarthy in Concepts of logical AI, 2000. http://www-formal.stanford.edu/jmc/concepts-ai/concepts-ai.html 10S3001-AI | Institut Teknologi Del 5 5 PS Agent and KB Agent Problem Solving Agent Knowledge-based Agent 10S3001-AI | Institut Teknologi Del 6 6 PS Agent and KB Agent Problem Solving Agent Knowledge-based Agent ▪ choose a solution among the available ▪ “smarter”. possibilities. ▪ The knowledge is very flexible. ▪ The knowledge is very specific and ▪ What he "knew" about the world inflexible. What he "knew" about the world does not evolve. evolve. ▪ can do reasoning for: ▪ problem solution (initial state, successor function, goal test). ▪ imperfect/partial information. ▪ choosing better action. 10S3001-AI | Institut Teknologi Del 7 7 Knowledge-based Agents ▪ Intelligent agents need knowledge about the world to choose good actions/decisions. ▪ Knowledge = 𝐬𝐞𝐧𝐭𝐞𝐧𝐜𝐞𝐬 in a knowledge representation language (formal language). ▪ A sentence is an assertion about the world. ▪ A knowledge-based agent is composed of: 1. Knowledge base: domain-specific content. 2. Inference mechanism: domain-independent algorithms Domain Algorithms {sentences} KB 10S3001-AI | Institut Teknologi Del 8 8 Knowledge-based Agents ▪ The agent must be able to: ▪ Represent states, actions, etc. ▪ Incorporate new percepts ▪ Update internal representations of the world ▪ Deduce hidden properties of the world ▪ Deduce appropriate actions ▪ Declarative approach to building an agent: ▪ Add new sentences: Tell it what it needs to know ▪ Query what is known: Ask itself what to do – answers should follow from the KB 10S3001-AI | Institut Teknologi Del 9 9 Knowledge-based Agents 10S3001-AI | Institut Teknologi Del 10 10  The Wumpus World 10S3001-AI | Institut Teknologi Del 11 11  The Wumpus World Gregory Yob (1975) 10S3001-AI | Institut Teknologi Del 12 These are all examples of pits and the Wumpus. So we have an agent that starts the room 1,1. And the mission of the agent is to navigate in this environment or the cave without being eaten or without falling into pits. There is some reward. It's possible for the agent to discover some gold and get it and get out of the cave. So there are some other components which is--that help the agent navigate in the cave. 12 The Wumpus World ▪ 4 X 4 grid of rooms ▪ Squares adjacent to Wumpus are smelly and squares adjacent to pit are breezy ▪ Glitter iff gold is in the same square ▪ Shooting kills Wumpus if you are facing it ▪ Wumpus emits a horrible scream when it is killed that can be heard anywhere ▪ Shooting uses up the only arrow ▪ Grabbing picks up gold if in same square ▪ Releasing drops the gold in same square 10S3001-AI | Institut Teknologi Del 13 13 Wumpus World PEAS ▪ Performance measure: ▪ gold +1000, death (eaten or falling in a pit) -1000, -1 per action taken, -10 for using the arrow. ▪ The games ends either when the agent dies or comes out of the cave. ▪ Environment ▪ 4 X 4 grid of rooms ▪ Agent starts in square [1,1] facing to the right ▪ Locations of the gold, and Wumpus are chosen randomly with a uniform distribution from all squares except [1,1] ▪ Each square other than the start can be a pit with probability of 0.2 ▪ Actuators: ▪ Left turn, Right turn, Forward, Grab, Release, Shoot ▪ Sensors: ▪ Stench, Breeze, Glitter, Bump, Scream ▪ Represented as a 5-element list ▪ Example: [Stench, Breeze, None, None, None] 10S3001-AI | Institut Teknologi Del 14 14 Wumpus World Environment ▪ Partially observable – only local perception ▪ Static – Wumpus and Pits do not move ▪ Discrete ▪ Single-agent – Wumpus is essentially a natural feature ▪ Deterministic – outcomes exactly specified ▪ Sequential – sequential at the level of actions 10S3001-AI | Institut Teknologi Del 15 15 Exploring Wumpus World ▪ Agent’s first steps: 10S3001-AI | Institut Teknologi Del 16 16 Exploring Wumpus World ▪ Agent’s later steps: 10S3001-AI | Institut Teknologi Del 17 17  Logical Agent 10S3001-AI | Institut Teknologi Del 18 18  Logic ▪ Knowledge base: a set of sentences in a formal representation, logic ▪ Logics: are formal languages for representing knowledge to extract conclusions ▪ Syntax: defines well-formed sentences in the language ▪ x + 2 ≥ y is a sentence ▪ x2 + y > is not a sentence ▪ Semantic: defines the truth or meaning of sentences in a world ▪ x + 2 ≥ y is true iff the number x + 2 is no less than the number y ▪ x + 2 ≥ y is true in a world where x = 7; y = 1 ▪ x + 2 ≥ y is false in a world where x = 0; y = 6 10S3001-AI | Institut Teknologi Del 19 As evoked earlier, logical agents needs a knowledge base. This is a set of sentences in the formal representation called logic. Logics are different forms, and are formal languages for representing knowledge to extract or to derive other conclusions. 19 Logic ▪ Inference: a procedure to derive a new sentence from other ones. ▪ Logical entailment: is a relationship between sentences. It means that a sentence follows logically from other sentences. Knowledge base KB entails sentence 𝛼 if and only if 𝛼 is true in all worlds where KB is true Notation: 𝐾𝐵 ⊨ 𝛼 10S3001-AI | Institut Teknologi Del 20 20 Entailment ▪ Example The KB containing “the shirt is green” and “the shirt is striped” entails “the shirt is green or the shirt is striped” ▪ Example x + y = 4 entails 4 = x + y 10S3001-AI | Institut Teknologi Del 21 21 Propositional Logic ▪ Propositional logic (PL) is the simplest logic. ▪ Syntax of PL: defines the allowable sentences or propositions. ▪ Definition (Proposition): A proposition is a declarative statement that’s either True or False. ▪ Atomic proposition: single proposition symbol. Each symbol is a proposition. Notation: upper case letters and may contain subscripts. ▪ Compound proposition: constructed from atomic propositions using parentheses and logical connectives. 10S3001-AI | Institut Teknologi Del 22 22 Atomic Proposition ▪ Examples of atomic propositions: ▪ 2 + 2 = 4 is a true proposition ▪ 𝑊1,3 is a proposition. It is true if there is a Wumpus in [1,3] ▪ “If there is a stench in [1,2] then there is a Wumpus in [1,3]” is a proposition ▪ “How are you?” or “Hello!” are not propositions. In general, statement that are questions, commands, or opinions are not propositions. 10S3001-AI | Institut Teknologi Del 23 23 Compound Proposition ▪ Examples of compound/complex propositions: Let 𝑝, 𝑝1 , and 𝑝2 be propositions ▪ Negation : ¬𝑝 is also a proposition. We call a literal either an atomic proposition or its negation. E.g., 𝑊1,3 is a positive literal, and ¬𝑊1,3 is a negative literal. ▪ Conjunction 𝑝1 ∧ 𝑝2. E.g., 𝑊1,3 ∧ 𝑃3,1 ▪ Disjunction 𝑝1 ∨ 𝑝2. E.g., 𝑊1,3 ∨ 𝑃3,1 ▪ Implication 𝑝1 ⇒ 𝑝2. E.g., 𝑊1,3 ∧ 𝑃3,1 ⇒ ¬𝑊2,2 ▪ If and only if 𝑝1 ⇔ 𝑝2. E.g., 𝑊1,3 ⇔ ¬𝑊2,2 10S3001-AI | Institut Teknologi Del 24 24  Truth Tables ▪ The semantics define the rules to determine the truth of a sentence. ▪ Semantics can be specified by truth tables. ▪ Boolean values domain: 𝑇, 𝐹 ▪ n-tuple: 𝑥1 , 𝑥2 , … , 𝑥𝑛 ▪ Operator on n-tuples : 𝑔 𝑥1 = 𝑣1 , 𝑥2 = 𝑣2 , … , 𝑥𝑛 = 𝑣𝑛 ▪ Definition: A truth table defines an operator 𝑔 on n-tuples by specifying a boolean value for each tuple ▪ Number of rows in a truth table? R = 2𝑛 10S3001-AI | Institut Teknologi Del 25 The number of rows in the truth table is 2𝑛 , where 𝑛 is a number of atomic propositions. 25  Building Propositions 10S3001-AI | Institut Teknologi Del 26 26 Building Propositions ▪ Negation: 𝒑 ¬𝒑 T F F T 𝒑 𝒒 𝒑∧𝒒 ▪ Conjunction: T T T T F F F T F F F F 10S3001-AI | Institut Teknologi Del 27 27 Building Propositions ▪ Disjunction: 𝒑 𝒒 𝒑∨𝒒 T T T T F T F T T F F F 𝒑 𝒒 𝒑⨁𝒒 ▪ Exclusive or: T T F T F T F T T F F F 10S3001-AI | Institut Teknologi Del 28 28 Building Propositions ▪ Implication: 𝒑 𝒒 𝒑⇒𝒒 T T T T F F F T T F F T 𝒑 𝒒 𝒑⟺𝒒 ▪ Biconditional or If and only if (IFF): T T T T F F F T F F F T 10S3001-AI | Institut Teknologi Del 29 29 Precedence of Operators ▪ Just like arithmetic operators, there is an operator precedence when evaluating logical operators as follows: 1. Expressions in parentheses are processed (inside to outside) 2. Negation 3. AND 4. OR 5. Implication 6. Biconditional 7. Left to right ▪ Use parentheses whenever you have any doubt! 10S3001-AI | Institut Teknologi Del 30 30 Building Propositions 𝒑 𝒒 𝒓 ¬𝒓 𝒑∨𝒒 𝒑 ∨ 𝒒 ⇒ ¬𝒓 T T T F T F T T F T T T T F T F T F T F F T T T F T T F T F F T F T T T F F T F F T F F F T F T 10S3001-AI | Institut Teknologi Del 31 31 Logical Equivalence ▪ Two propositions 𝑝 and 𝑞 are logically equivalent if and only if the columns in the truth table giving their truth values agree. ▪ We write this as 𝑝 ⇔ 𝑞 or 𝑝 ≡ 𝑞. 𝒑 𝒒 ¬𝒑 ¬𝒑 ∨ 𝒒 𝒑⇒𝒒 T T F T T T F F F F F T T T T F F T T T 10S3001-AI | Institut Teknologi Del 32 32 Properties of Operators ▪ 𝑝∧𝑞 ≡ 𝑞∧𝑝 commutativity of ∧ ▪ 𝑝∨𝑞 ≡ 𝑞∨𝑝 commutativity of ∨ ▪ 𝑝∧𝑞 ∧𝑟 ≡ 𝑝∧ 𝑞∧𝑟 associativity of ∧ ▪ 𝑝∨𝑞 ∨𝑟 ≡ 𝑝∨ 𝑞∨𝑟 associativity of ∨ ▪ 𝑝 ∧ 𝑇𝑟𝑢𝑒 ≡ 𝑝 identity element ▪ 𝑝 ∨ 𝑇𝑟𝑢𝑒 ≡ 𝑇𝑟𝑢𝑒 identity element ▪ ¬ ¬𝑝 ≡ 𝑝 double-negation elimination ▪ 𝑝∧𝑝 ≡ 𝑝 idempotence for ∧ ▪ 𝑝∨𝑝 ≡ 𝑝 idempotence for ∨ ▪ 𝑝∧ 𝑞∨𝑟 ≡ 𝑝∧𝑞 ∨ 𝑝∧𝑟 distributivity of ∧ over ∨ ▪ 𝑝∨ 𝑞∧𝑟 ≡ 𝑝∨𝑞 ∧ 𝑝∨𝑟 distributivity of ∨ over ∧ ▪ 𝑝 ∧ ¬𝑝 ≡ 𝐹𝑎𝑙𝑠𝑒 and 𝑝 ∨ ¬𝑝 ≡ 𝑇𝑟𝑢𝑒 ▪ ¬ 𝑝 ∧ 𝑞 ≡ ¬𝑝 ∨ ¬𝑞 de Morgan’s laws ▪ ¬ 𝑝 ∨ 𝑞 ≡ ¬𝑝 ∧ ¬𝑞 de Morgan’s laws 10S3001-AI | Institut Teknologi Del 33 33 Tautology and Contradiction ▪ Tautology is a proposition which is always true ▪ Contradiction is a proposition which is always false ▪ Contingency is a proposition which is neither a tautology or a contradiction 𝒑 ¬𝒑 𝒑 ∨ ¬𝒑 𝒑 ∧ ¬𝒑 T F T F F T T F 10S3001-AI | Institut Teknologi Del 34 34 Contrapositive, Inverse, etc. ▪ Given an implication 𝑝 ⇒ 𝑞 ▪ The converse is: 𝑞 ⇒ 𝑝 ▪ The contrapositive is: ¬𝑞 ⇒ ¬𝑝 ▪ The inverse is: ¬𝑝 ⇒ ¬𝑞 10S3001-AI | Institut Teknologi Del 35 35  Contrapositive, Inverse, etc. ▪ Given an implication 𝑝 ⇒ 𝑞 ▪ The converse is: 𝑞 ⇒ 𝑝 ▪ The contrapositive is: ¬𝑞 ⇒ ¬𝑝 ▪ The inverse is: ¬𝑝 ⇒ ¬𝑞 Example: Hot is a sufficient condition for my going to the beach. ▪ The implication is: ℎ𝑜𝑡 ⇒ 𝑏𝑒𝑎𝑐ℎ ▪ The converse is: 𝑏𝑒𝑎𝑐ℎ ⇒ ℎ𝑜𝑡 ▪ The contrapositive is:¬𝑏𝑒𝑎𝑐ℎ ⇒ ¬ℎ𝑜𝑡 ▪ The inverse is:¬ℎ𝑜𝑡 ⇒ ¬𝑏𝑒𝑎𝑐ℎ 10S3001-AI | Institut Teknologi Del 36 Among the connectives, the implication plays a crucial role in inference. Let's see first it's different variants and also clarify the terminology. So first of all, an implication is a Boolean expression, or actually, a proposition of the form p implies q. So sometimes you would see it written as p implies q, but this is the same. 36  Inference Rules 10S3001-AI | Institut Teknologi Del 37 37 Inference (Modus Ponens) 𝑝 𝑝⇒𝑞 𝑞 𝑤𝑎𝑟𝑚 𝑤𝑎𝑟𝑚 ⇒ 𝑠𝑢𝑛𝑛𝑦 𝑠𝑢𝑛𝑛𝑦 10S3001-AI | Institut Teknologi Del 38 38  Inference (Modus Ponens) ▪ Horn clauses: a proposition of the form: 𝑝1 ∧ ⋯ ∧ 𝑝𝑛 ⇒ 𝑞 ▪ Modus Ponens deals with Horn clauses: 𝑝1 , … , 𝑝𝑛 𝑝1 ∧ ⋯ ∧ 𝑝𝑛 ⇒ 𝑞 𝑞 10S3001-AI | Institut Teknologi Del 39 Modus Ponens can be extended by handling what we call Horn clauses It's a proposition of the form p1, and p2, and pn implies q. 39 Inference (Modus Tollens) ¬𝑞 𝑝⇒𝑞 ¬𝑝 ¬𝑏𝑒𝑎𝑐ℎ ℎ𝑜𝑡 ⇒ 𝑏𝑒𝑎𝑐ℎ ¬ℎ𝑜𝑡 10S3001-AI | Institut Teknologi Del 40 40 Common Rules 10S3001-AI | Institut Teknologi Del 41 41 Truth Tables for Connectives ▪ Summary: 10S3001-AI | Institut Teknologi Del 42 42  Reduced Wumpus World 10S3001-AI | Institut Teknologi Del 43 43 Wumpus World KB Let’s build the KB for the reduced Wumpus world. ▪ Let 𝑃𝑖,𝑗 be true if there is a pit in 𝑖, 𝑗 agent mulai ▪ Let 𝐵𝑖,𝑗 be true if there is a breeze in 𝑖, 𝑗 dari posisi 𝑅1 : ¬𝑃1,1 (1,1): ruangan aman ▪ “A square is breezy if and only if there is an adjacent pit” 𝑅2 : 𝐵1,1 ⇔ 𝑃1,2 ∨ 𝑃2,1 𝑅3 : 𝐵2,1 ⇔ 𝑃1,1 ∨ 𝑃2,2 ∨ 𝑃3,1 tidak ada pit di 1,1 𝑅4 : ¬𝐵1,1 𝑅5 : 𝐵2,1 gunakan simbol propositional logic Questions: Based on this KB, is 𝐾𝐵 ⊨ 𝑃1,2? Is 𝐾𝐵 ⊨ 𝑃2,2 ? 10S3001-AI | Institut Teknologi Del 44 44  Wumpus World KB Let’s build the KB for the reduced Wumpus world. ▪ Let 𝑃𝑖,𝑗 be true if there is a pit in 𝑖, 𝑗 ▪ Let 𝐵𝑖,𝑗 be true if there is a breeze in 𝑖, 𝑗 𝑅1 : ¬𝑃1,1 ▪ “A square is breezy if and only if there is an adjacent pit” 𝑅2 : 𝐵1,1 ⇔ 𝑃1,2 ∨ 𝑃2,1 𝑅3 : 𝐵2,1 ⇔ 𝑃1,1 ∨ 𝑃2,2 ∨ 𝑃3,1 𝑅4 : ¬𝐵1,1 𝑅5 : 𝐵2,1 Questions: Based on this KB, is 𝐾𝐵 ⊨ 𝑃1,2? Is 𝐾𝐵 ⊨ 𝑃2,2 ? 10S3001-AI | Institut Teknologi Del 45 For example we could wonder whether there is a pit in 1,2. In other words, does KB entails 𝑃1,2 , and does KB entails 𝑃2,2 ? 45  Entailment and Inference ▪ Semantics: Determine entailment by Model Checking, that is enumerate all models and show that the sentence α must hold in all models. 𝐾𝐵 ⊨ 𝛼 ▪ Syntax: Determine entailment by Theorem Proving, that is apply rules of inference to KB to build a proof of α without enumerating and checking all models. 𝐾𝐵 ⊢ 𝛼 ▪ But how are entailment and inference related? *) Jika knowledge base ‘KB’ entails ‘𝛼’ maka semua interpretasi (baik menetapkan nilai 'benar' atau 'salah' ke variabel) yang mengevaluasi knowledge Anda ke True, juga mengevaluasi 𝛼 ke True. 𝐾𝐵 ⊨ 𝛼. *) Inferensi adalah prosedur untuk menurunkan kalimat baru '𝛼' dari 'KB' mengikuti beberapa algoritma. 𝐾𝐵 ⊢ 𝛼. 10S3001-AI | Institut Teknologi Del 46 It's important to take a break here to express again entailments and inferences in terms of semantic and syntax. Semantics goes along with entailment. Entailment means determining, whether by model checking, a sentence alpha must be be true, or must hold, in all models in which KB is true. So we'll have to write it as KB models alpha, means that is alpha true whenever KB is true. The syntax goes along with inference. And you know we like to determine entailment by what we call theorem proving. That is apply rule of inferences to the knowledge base to build a proof of alpha without having to explicitly enumerate all possible models or all truth tables for KB and for alpha. So we'll have to write this as either KB implies alpha, or KB infers alpha. In the semantics we talk about truth tables, models. And in syntax we talk about inference rules, et cetera. 46  Soundness & Completeness ▪ We want an inference algorithm that is: 1. Sound: does not infer false formulas, that is, derives only entailed sentences. 𝛼|𝐾𝐵 ⊢ 𝛼 ⊆ 𝐾𝐵 ⊨ 𝛼 2. Complete: derives ALL entailed sentences. 𝛼|𝐾𝐵 ⊢ 𝛼 ⊇ 𝐾𝐵 ⊨ 𝛼 inferred entailed formula formula 10S3001-AI | Institut Teknologi Del 47 ⊆ : subset of or equal to In other words, for inference algorithm to be sound means that we want all provable formulas, or propositions, to be actually true. In other words, for inference algorithm to be complete means that all true propositions must be provable using the inference algorithm. 47 Validity & Satisfiability ▪ A sentence is valid (aka tautology) if it is true in all models, e.g., 𝑇𝑟𝑢𝑒, 𝑝 ∨ ¬𝑝, 𝑝 ⇒ 𝑝, 𝑝 ∧ 𝑝 ⇒ 𝑞 ⇒𝑞 ▪ Validity is connected to inference via the Deduction Theorem: 𝐾𝐵 ⊨ 𝛼 𝐼𝐹𝐹 𝐾𝐵 ⇒ 𝛼 is valid ▪ A sentence is satisfiable if it is true in some model e.g., 𝑝 ∨ 𝑞, 𝑟 ▪ A sentence is unsatisfiable if it is true in no models e.g., 𝑝 ∧ ¬𝑝 ▪ Satisfiability is connected to inference via the following: 𝐾𝐵 ⊨ 𝛼 𝐼𝐹𝐹 𝐾𝐵 ∧ ¬𝛼 is unsatisfiable i.e., prove α by contradiction 10S3001-AI | Institut Teknologi Del 48 48 Determining Entailment how to determine entailments? ▪ Given a Knowledge Base (KB) (set of sentences in PL), given a query α, output whether KB entails 𝛼, noted: 𝐾𝐵 ⊨ 𝛼 ▪ We will see two ways of doing proofs in PL: ▪ Model checking enumerate the models (truth table enumeration, exponential). ▪ Application of inference rules (proof checking/theorem proving): Syntactic derivations with rules like Modus Ponens (Backward chaining and forward chaining). A proof is a sequence of inference rule applications. 10S3001-AI | Institut Teknologi Del 49 49  Model Checking and Inference 10S3001-AI | Institut Teknologi Del 50 50  Model Checking ▪ Truth Table for inference ▪ Model: assignment 𝑇/𝐹 to every propositional symbol. ▪ Check that 𝛼 is true in every model in which KB is true. 10S3001-AI | Institut Teknologi Del 51 Here we are going to enumerate all possible models using truth tables. 51 Model Checking a set of seven propositional symbols ▪ Truth Table for inference a set of five rules ▪ Model: assignment 𝑇/𝐹 to every propositional symbol. ▪ Check that 𝛼 is true in every model in which KB is true. 27 = 128 The set of rules, built in the knowledge base to represent the reduced Wumpus world 10S3001-AI | Institut Teknologi Del 52 52 Model Checking a set of seven propositional symbols ▪ Truth Table for inference a set of five rules ▪ Model: assignment 𝑇/𝐹 to every propositional symbol. ▪ Check that 𝛼 is true in every model in which KB is true. jika hanya menggunakan ini 27 = 128 The set of rules, built in the knowledge base to represent the reduced Wumpus world 10S3001-AI | Institut Teknologi Del 53 𝐾𝐵 ⊨ 𝑃1,2 ? 𝐾𝐵 ⊨ ¬𝑃1,2 𝐾𝐵 ⊨ 𝑃2,2 ? 53  Inference: Wumpus World 𝑅1 : ¬𝑃1,1 𝐾𝐵 ⊨ 𝑃1,2 ? 𝐾𝐵 ⊨ 𝑃2,1 ? 𝑅2 : 𝐵1,1 ⇔ 𝑃1,2 ∨ 𝑃2,1 𝑅3 : 𝐵2,1 ⇔ 𝑃1,1 ∨ 𝑃2,2 ∨ 𝑃3,1 𝑅2 : 𝐵1,1 ⇔ 𝑃1,2 ∨ 𝑃2,1 𝑅4 : ¬𝐵1,1 ⇔ 𝑅5 : 𝐵2,1 𝑅6 : 𝐵1,1 ⇒ 𝑃1,2 ∨ 𝑃2,1 ∧ 𝑃1,2 ∨ 𝑃2,1 ⇒ 𝐵1,1 ∧ 𝑃1,2 ∨ 𝑃2,1 ⇒ 𝐵1,1 𝐶𝑜𝑛𝑡𝑟𝑎𝑝. ¬𝐵1,1 ⇒ ¬ 𝑃1,2 ∨ 𝑃2,1 𝑑𝑒 𝑀𝑜𝑟𝑔𝑎𝑛′ 𝑠 𝐿𝑎𝑤 𝑅4 : ¬𝐵1,1 ¬𝐵1,1 ⇒ ¬𝑃1,2 ∧ ¬𝑃2,1 𝑀𝑜𝑑𝑢𝑠 𝑃𝑜𝑛𝑒𝑛 ¬𝑃1,2 ∧ ¬𝑃2,1 ∧ ¬𝑃1,2 ¬𝑃2,1 10S3001-AI | Institut Teknologi Del 𝐾𝐵 ⊨ ¬𝑃1,2 𝐾𝐵 ⊨ ¬𝑃2,1 54 Now suppose we don't have model checking as a tool, we only can do inference using Modus Ponens and whatever equivalence propositional logic formula we found earlier. As we can see, no semantics at all, just syntax. 54  Inference As A Search Problem ▪ Initial state: The initial KB ▪ Actions: all inference rules applied to all sentences that match the top of the inference rule ▪ Results: add the sentence in the bottom half of the inference rule ▪ Goal: a state containing the sentence we are trying to prove. 𝐾𝐵 ⊨ 𝑃1,2 ? 10S3001-AI | Institut Teknologi Del 55 You might have noticed something from the previous example, which is that inference sounds like search. On we're searching through what rules to apply, what inference to do to achieve some goal, which is to put entailments between the knowledge base and the proposition. So it's possible actually to cast the problem of inference as a search problem and use any of the algorithms we have seen in the previous weeks. So… Initial state: The initial KB Actions: all inference rules applied to all sentences that match the top of the inference rule Results: add the sentence in the bottom half of the inference rule Goal: a state containing the sentence we are trying to prove. 55  Theorem Proving and Proof by Resolution 10S3001-AI | Institut Teknologi Del 56 56  Theorem Proving ▪ Search for proofs is a more efficient way than enumerating models (We can ignore irrelevant information) ▪ Truth tables have an exponential number of models. ▪ The idea of inference is to repeat applying inference rules to the KB. ▪ Inference can be applied whenever suitable premises are found in the KB. ▪ Inference is sound. How about completeness? 10S3001-AI | Institut Teknologi Del 57 Search for proofs is a more efficient way than enumerating models. Why? The main reason is that, first of all, truth tables are exponentials, and the number of propositions. And furthermore, when we do inference, we can simply ignore irrelevant information. 57 Theorem Proving ▪ Two ways to ensure completeness: ▪ Proof by resolution: use powerful inference rules (resolution rule) ▪ Forward or Backward chaining: use of modus ponens on a restricted form of propositions (Horn clauses) ▪ Resolution: ONE single inference rule ▪ Invented by Robinson, 1965 ▪ Resolution + Search = complete inference algorithm. 10S3001-AI | Institut Teknologi Del 58 58 Proof by Resolution ▪ Resolution & Wumpus world: 10S3001-AI | Institut Teknologi Del 59 59 Proof by Resolution ▪ Unit resolution: 𝑙1 ∨ ⋯ ∨ 𝑙𝑘 𝑚 𝑙1 ∨ ⋯ ∨ 𝑙𝑖−1 ∨ 𝑙𝑖+1 ∨ ⋯ ∨ 𝑙𝑘 where 𝑙𝑖 and 𝑚 are complementary literals. ▪ Example: 𝑃1,3 ∨ 𝑃2,2 ¬𝑃2,2 𝑃1,3 ▪ We call a clause a disjunction of literals. ▪ Unit resolution: Clause + Literal = New clause. 10S3001-AI | Institut Teknologi Del 60 60 Proof by Resolution ▪ Resolution inference rule (for CNF): 𝑙1 ∨ ⋯ ∨ 𝑙𝑘 𝑚1 ∨ ⋯ ∨ 𝑚𝑛 𝑙1 ∨ ⋯ ∨ 𝑙𝑖−1 ∨ 𝑙𝑖+1 ∨ ⋯ ∨ 𝑙𝑘 ∨ 𝑚1 ∨ ⋯ ∨ 𝑚𝑗−1 ∨ 𝑚𝑗+1 ∨ ⋯ ∨ 𝑚𝑛 where 𝑙𝑖 and 𝑚𝑗 are complementary literals. ▪ Resolution applies only to clauses ▪ Fact: Every sentence in PL is logically equivalent to a conjunction of clauses. ▪ Conjunctive Normal Form (CNF): Conjunction of disjunction of literals: ▪ Example: 𝐴 ∨ ¬𝐵 ∧ 𝐵 ∨ ¬𝐶 ∨ ¬𝐷 ▪ Resolution inference rule (for CNF): sound and complete for propositional logic 10S3001-AI | Institut Teknologi Del 61 61  Conversion to CNF and Resolution Algorithm 10S3001-AI | Institut Teknologi Del 62 62 Conversion to CNF 𝐵1,1 ⇔ 𝑃1,2 ∨ 𝑃2,1 1. Eliminate ⇔, replacing 𝛼 ⇔ 𝛽 with 𝛼 ⇒ 𝛽 ∧ 𝛽 ⇒ 𝛼. 𝐵1,1 ⇒ 𝑃1,2 ∨ 𝑃2,1 ∧ 𝑃1,2 ∨ 𝑃2,1 ⇒ 𝐵1,1 2. Eliminate ⇒, replacing 𝛼 ⇒ 𝛽 with ¬𝛼 ∨ 𝛽. ¬𝐵1,1 ∨ 𝑃1,2 ∨ 𝑃2,1 ∧ ¬ 𝑃1,2 ∨ 𝑃2,1 ∨ 𝐵1,1 3. Move ¬ inwards using de Morgans rules and double-negation: ¬𝐵1,1 ∨ 𝑃1,2 ∨ 𝑃2,1 ∧ ¬𝑃1,2 ∧ ¬𝑃2,1 ∨ 𝐵1,1 4. Apply distributivity law (∨ over ∧) and flatten: ¬𝐵1,1 ∨ 𝑃1,2 ∨ 𝑃2,1 ∧ ¬𝑃1,2 ∨ 𝐵1,1 ∧ ¬𝑃2,1 ∨ 𝐵1,1 10S3001-AI | Institut Teknologi Del 63 63 Resolution Algorithm 10S3001-AI | Institut Teknologi Del 64 64 Resolution Example 𝐾𝐵 = 𝑅4 ∧ 𝑅2 = 𝐵1,1 ⇔ 𝑃1,2 ∨ 𝑃2,1 ∧ ¬𝐵1,1 𝛼 = ¬𝑃1,2 10S3001-AI | Institut Teknologi Del 65 65  Forward and Backward Chaining 10S3001-AI | Institut Teknologi Del 66 66 Forward/Backward Chaining ▪ KB = conjunction of Horn clauses ▪ Horn clauses: logic proposition of the form: 𝑝1 ∧ ⋯ ∧ 𝑝𝑛 ⇒ 𝑞 ▪ Modus Ponens (for Horn Form): complete for Horn KBs 𝑝1 , ⋯ , 𝑝𝑛 𝑝1 ∧ ⋯ ∧ 𝑝𝑛 ⇒ 𝑞 𝑞 ▪ Can be used with forward chaining or backward chaining. ▪ These algorithms are very natural and run in linear time 10S3001-AI | Institut Teknologi Del 67 67 Forward Chaining ▪ Idea: Fire any rule whose premises are satisfied in the KB, add its conclusion to the 𝐾𝐵, until query is found. ▪ This proves that 𝐾𝐵 ⇒ 𝑄 is true in all possible worlds (i.e. trivial), and hence it proves entailment. ▪ Forward Chaining is sound and complete for Horn KB 10S3001-AI | Institut Teknologi Del 68 68 Forward Chaining Example Note: “OR” Gate Perhatikan 𝐾𝐵, 𝐿 didapatkan baik dari rule ke-5 maupun rule-6, itulah sebabnya “OR” Gate digambarkan sebelum node 𝐿. “AND” Gate 10S3001-AI | Institut Teknologi Del 69 69 Forward Chaining Example 10S3001-AI | Institut Teknologi Del 70 70 Forward Chaining Example 10S3001-AI | Institut Teknologi Del 71 71 Forward Chaining Example 10S3001-AI | Institut Teknologi Del 72 72 Forward Chaining Example 10S3001-AI | Institut Teknologi Del 73 73 Forward Chaining Example 10S3001-AI | Institut Teknologi Del 74 74 Forward Chaining Example 10S3001-AI | Institut Teknologi Del 75 75 Forward Chaining Example 10S3001-AI | Institut Teknologi Del 76 76 Backward Chaining ▪ Idea: Works backwards from the query 𝑞 ▪ to prove 𝑞 by Backward Chaining (BC): ▪ Check if 𝑞 is known already, or ▪ Prove by BC all premises of some rule concluding 𝑞 ▪ Hence BC maintains a stack of sub-goals that need to be proved to get to 𝑞 ▪ Avoid loops: check if new sub-goal is already on the goal stack ▪ Avoid repeated work: check if new sub-goal ▪ has already been proved true, or ▪ has already failed 10S3001-AI | Institut Teknologi Del 77 77 Backward Chaining Example Note: The idea is to go down in the graph until it reaches the facts here, 𝐴 and 𝐵, and bring that information up. 10S3001-AI | Institut Teknologi Del 78 78 Backward Chaining Example 10S3001-AI | Institut Teknologi Del 79 79 Backward Chaining Example 10S3001-AI | Institut Teknologi Del 80 80 Backward Chaining Example Note: Kita perlu 𝑃 untuk membuktikan 𝐿 dan 𝐿 untuk membuktikan 𝑃 10S3001-AI | Institut Teknologi Del 81 81 Backward Chaining Example Note: As soon as you can move forward, do so. 10S3001-AI | Institut Teknologi Del 82 82 Backward Chaining Example 10S3001-AI | Institut Teknologi Del 83 83 Backward Chaining Example 10S3001-AI | Institut Teknologi Del 84 84 Backward Chaining Example 10S3001-AI | Institut Teknologi Del 85 85 Backward Chaining Example 10S3001-AI | Institut Teknologi Del 86 86 Backward Chaining Example 10S3001-AI | Institut Teknologi Del 87 87 Forward vs. Backward ▪ Forward chaining is data-driven, automatic, unconscious processing, ▪ e.g., object recognition, routine decisions ▪ May do lots of work that is irrelevant to the goal ▪ Backward chaining is goal-driven, appropriate for problem-solving, ▪ e.g., Where are my keys? How do I get into a PhD program? ▪ Complexity of BC can be much less than linear in size of KB 10S3001-AI | Institut Teknologi Del 88 88 Limits of Propositional Logic ▪ Limits of PL? ▪ PL is not expressive enough to describe all the world around us. It can’t express information about different object and the relation between objects. ▪ PL is not compact. It can’t express a fact for a set of objects without enumerating all of them which is sometimes impossible. ▪ Example: We have a vacuum cleaner (Roomba) to clean a 10 × 10 squares in the classroom. Use PL to express information about the squares. 10S3001-AI | Institut Teknologi Del 89 89 Limits of Propositional Logic ▪ The proposition 𝑠𝑞𝑢𝑎𝑟𝑒1 _is_clean expresses information about square1 being clean. How can one write this in a less heavy way? ▪ How can we express that all squares in the room are clean? ▪ How can we express that some squares in the room are clean? ▪ How can we express that some squares have chairs on them? 10S3001-AI | Institut Teknologi Del 90 90 Summary ▪ Logical agents apply inference to a knowledge base to derive new information and make decisions ▪ Basic concepts of logic: ▪ Syntax: formal structure of sentences ▪ Semantics: truth of sentences wrt models ▪ Entailment: necessary truth of one sentence given another ▪ Inference: deriving sentences from other sentences ▪ Soundness: derivations produce only entailed sentences ▪ Completeness: derivations can produce all entailed sentences 10S3001-AI | Institut Teknologi Del 91 91 Summary ▪ Wumpus world requires the ability to represent partial and negated information, reason by cases, etc. ▪ Forward, backward chaining are linear in time, complete for Horn clauses. ▪ Resolution is sound and complete for propositional logic. ▪ Propositional logic lacks expressive power. 10S3001-AI | Institut Teknologi Del 92 92 References ▪ S. J. Russell and P. Borvig, Artificial Intelligence: A Modern Approach (4th Edition), Prentice Hall International, 2020. ▪ Kevin C. Klement, “Propositional Logic”, https://www.iep.utm.edu/prop-log/. ▪ AITopics: An official publication of the Association for the Advancement of Artificial Intelligence (AAAI), https://aitopics.org/search. 10S3001-AI | Institut Teknologi Del 93 93  eof 10S3001-AI | Institut Teknologi Del 94 94