First Order Logic PDF

First Order Logic 10S3001 – Artificial Intelligence Samuel I. G. Situmeang Faculty of Informatics and Electrical Engineering 1  Objectives Students are able: ▪ to explain the concept of first-order logic clearly....

First Order Logic 10S3001 – Artificial Intelligence Samuel I. G. Situmeang Faculty of Informatics and Electrical Engineering 1  Objectives Students are able: ▪ to explain the concept of first-order logic clearly. ▪ to apply inference to first-order logic propositions by using first-order logic inference rules. ▪ to apply unification to first-order logic propositions correctly. 10S3001-AI | Institut Teknologi Del 2 Siswa mampu: untuk menjabarkan konsep first-order logic dengan jelas. untuk menerapkan inferensi pada proposisi first-order logic dengan menggunakan aturan inferensi logika first-order logic. untuk menerapkan unifikasi pada proposisi first-order logic dengan tepat. 2 First Order Logic Representation Of Language ▪ Whorf (1956) suggest that communities determine lang. categories ▪ Wanner (1975) subject remember the content of what they read better than the actual words. ▪ Mitchell et al. (2008) could predict –with above chance accuracy– the areas of the brain that would activate with certain words(fMRI) 10S3001-AI | Institut Teknologi Del 3 3 First Order Logic Formal/Natural Languages ▪ Objects (cat, dog, house, John, etc.) ▪ Relations (has color, bigger than, comes between, etc.) ▪ Facts: (One value for a given input: has father, has head, can swim) Facts have a truth value. true or false 10S3001-AI | Institut Teknologi Del 4 4 Formal Languages Ontological and Epistemological Commitments Language Ontological Commitment1 Epistemological Commitment2 Propositional Logic facts true/false/unknown First-Order Logic facts, objects, relations true/false/unknown Temporal Logic facts,objects, relations, time true/false/unknown Probability Theory facts degree of belief 2 [0, 1] Fuzzy Logic facts with degree of truth known interval value 1What exists in the world 2Agent’s beliefs about facts 10S3001-AI | Institut Teknologi Del 5 5 Relationships Models for first order logic 10S3001-AI | Institut Teknologi Del 6 6 First Order Logic Syntax Sentence → AtomicSentence | ComplexSentence AtomicSentence → Predicate | Predicate(Term,...) | Term = Term ComplexSentence → (Sentence) | [Sentence] | ¬ Sentence | Sentence ∧ Sentence | Sentence ∨ Sentence | Sentence  Sentence | Sentence  Sentence | Quantifier Variable,... Sentence Term → Function(Term,... ) | Constant | Variable Quantifier → | Constant → A | X1 | John |... Variable → a|x|s|... Predicate → True | False | After | Loves | Raining |... Function → Mother | Left leg |... Operator Precedence3 : ¬, ∧, ∨, ,  3Otherwise the grammar is ambiguous 10S3001-AI | Institut Teknologi Del 7 7 First Order Logic Syntax ▪ Three kinds of symbols ▪ Constant: objects ▪ Predicate: relations ▪ Function: functions (i.e. can return values other than truth vals.) ▪ Predicate and Function have arity ▪ Symbols have an interpretation ▪ Terms: 𝐿𝑒𝑓𝑡𝐿𝑒𝑔(𝐽𝑜ℎ𝑛) ▪ Atomic Sentences state facts: 𝐵𝑟𝑜𝑡ℎ𝑒𝑟(𝑅𝑖𝑐ℎ𝑎𝑟𝑑, 𝐽𝑜ℎ𝑛) ▪ Complex Sentence: 𝐵𝑟𝑜𝑡ℎ𝑒𝑟(𝑅, 𝐽) ∧ 𝐵𝑟𝑜𝑡ℎ𝑒𝑟(𝐽, 𝑅) 𝑜𝑟 ¬𝐾𝑖𝑛𝑔(𝑅𝑖𝑐ℎ𝑎𝑟𝑑)  𝐾𝑖𝑛𝑔(𝐽𝑜ℎ𝑛) ▪ Universal Quantifiers: 𝐾𝑖𝑛𝑔(𝑥)  𝑃𝑒𝑟𝑠𝑜𝑛(𝑥) ▪ Existential Quantifiers: 𝐶𝑟𝑜𝑤𝑛(𝑥) ∧ 𝑂𝑛𝐻𝑒𝑎𝑑(𝑥, 𝐽𝑜ℎ𝑛) 10S3001-AI | Institut Teknologi Del 8 8 First Order Logic Try this What is the interpretation for: ▪ 𝐾𝑖𝑛𝑔(𝑅𝑖𝑐ℎ𝑎𝑟𝑑) ∨ 𝐾𝑖𝑛𝑔(𝐽𝑜ℎ𝑛) ▪ ¬𝐵𝑟𝑜𝑡ℎ𝑒𝑟(𝐿𝑒𝑓𝑡𝐿𝑒𝑔(𝑅𝑖𝑐ℎ𝑎𝑟𝑑), 𝐽𝑜ℎ𝑛) ▪ 𝑥𝑦 𝐵𝑟𝑜𝑡ℎ𝑒𝑟(𝑥, 𝑦)  𝑆𝑖𝑏𝑙𝑖𝑛𝑔(𝑥, 𝑦) ▪ 𝐼𝑛(𝑃𝑎𝑟𝑖𝑠, 𝐹𝑟𝑎𝑛𝑐𝑒) ∧ 𝐼𝑛(𝑀𝑎𝑟𝑠𝑒𝑖𝑙𝑙𝑒𝑠, 𝐹𝑟𝑎𝑛𝑐𝑒) ▪ 𝑐 𝐶𝑜𝑢𝑛𝑡𝑟𝑦(𝑐) ∧ 𝐵𝑜𝑟𝑑𝑒𝑟(𝑐, 𝐸𝑐𝑢𝑎𝑑𝑜𝑟)  𝐼𝑛(𝑐, 𝑆𝑜𝑢𝑡ℎ𝐴𝑚𝑒𝑟𝑖𝑐𝑎) ▪  𝐶𝑜𝑢𝑛𝑡𝑟𝑦(𝑐) ∧ 𝐵𝑜𝑟𝑑𝑒𝑟(𝑐, 𝑆𝑝𝑎𝑖𝑛) ∧ 𝐵𝑜𝑟𝑑𝑒𝑟(𝑐, 𝐼𝑡𝑎𝑙𝑦) 10S3001-AI | Institut Teknologi Del 9 9 First Order Logic More Facts ▪ Richard has only two brothers, John and Geoffrey 𝐵𝑟𝑜𝑡ℎ𝑒𝑟 𝐽𝑜ℎ𝑛, 𝑅𝑖𝑐ℎ𝑎𝑟𝑑 ∧ 𝐵𝑟𝑜𝑡ℎ𝑒𝑟 𝐺𝑒𝑜𝑓𝑓𝑟𝑒𝑦, 𝑅𝑖𝑐ℎ𝑎𝑟𝑑 ∧ 𝐽𝑜ℎ𝑛  𝑥 𝐵𝑟𝑜𝑡ℎ𝑒𝑟 𝑥, 𝑅𝑖𝑐ℎ𝑎𝑟𝑑  𝑥 = 𝐽𝑜ℎ𝑛 ∨ 𝑥 = 𝐺𝑒𝑜𝑓𝑓𝑟𝑒𝑦 ▪ No Region in South America borders any region in Europe 𝑐, 𝑑 𝐼𝑛 𝑐, 𝑆𝑜𝑢𝑡ℎ𝐴𝑚𝑒𝑟𝑖𝑐𝑎 ∧ 𝐼𝑛 𝑑, 𝐸𝑢𝑟𝑜𝑝𝑒  ¬𝐵𝑜𝑟𝑑𝑒𝑟 𝑐, 𝑑 ▪ No two adjacent countries have the same map color 𝑥, 𝑦 𝐶𝑜𝑢𝑛𝑡𝑟𝑦 𝑥 ∧ 𝐶𝑜𝑢𝑛𝑡𝑟𝑦 𝑦 ∧ 𝐵𝑜𝑟𝑑𝑒𝑟 𝑥, 𝑦  ¬ 𝐶𝑜𝑙𝑜𝑟 𝑥 = 𝐶𝑜𝑙𝑜𝑟 𝑦 ∧ ¬ 𝑥 = 𝑦 10S3001-AI | Institut Teknologi Del 10 10 Assertions and Queries in FOL ASK and TELL ▪ 𝑇𝐸𝐿𝐿(𝐾𝐵, 𝐾𝑖𝑛𝑔(𝐽𝑜ℎ𝑛)) ▪ 𝑇𝐸𝐿𝐿(𝐾𝐵, 𝑥 𝐾𝑖𝑛𝑔(𝑥)  𝑃𝑒𝑟𝑠𝑜𝑛(𝑥)) ▪ 𝐴𝑆𝐾(𝐾𝐵, 𝐾𝑖𝑛𝑔(𝐽𝑜ℎ𝑛)) return True ▪ 𝐴𝑆𝐾(𝐾𝐵, 𝑥 𝑃𝑒𝑟𝑠𝑜𝑛(𝑥)) return True ▪ 𝐴𝑆𝐾𝑉𝐴𝑅𝑆(𝐾𝐵, 𝑃𝑒𝑟𝑠𝑜𝑛(𝑥)) yields {𝑥/𝐽𝑜ℎ𝑛, 𝑥/𝑅𝑖𝑐ℎ𝑎𝑟𝑑}, a binding list 10S3001-AI | Institut Teknologi Del 11 11 First Order Logic Kinship "The son of my father is my brother", "One's grandmother is the mother of one's parent", etc. ▪ Domain: People ▪ Unary predicates: 𝑀𝑎𝑙𝑒, 𝐹𝑒𝑚𝑎𝑙𝑒 ▪ Relations: 𝑃𝑎𝑟𝑒𝑛𝑡, 𝑆𝑖𝑏𝑙𝑖𝑛𝑔, 𝐵𝑟𝑜𝑡ℎ𝑒𝑟, 𝑆𝑖𝑠𝑡𝑒𝑟, 𝐶ℎ𝑖𝑙𝑑, 𝐷𝑎𝑢𝑔ℎ𝑡𝑒𝑟, 𝑆𝑜𝑛, 𝑆𝑝𝑜𝑢𝑠𝑒, 𝑊𝑖𝑓𝑒, 𝐻𝑢𝑠𝑏𝑎𝑛𝑑, 𝐺𝑟𝑎𝑛𝑑𝑝𝑎𝑟𝑒𝑛𝑡, 𝐺𝑟𝑎𝑛𝑑𝑐ℎ𝑖𝑙𝑑, 𝐶𝑜𝑢𝑠𝑖𝑛, 𝐴𝑢𝑛𝑡, 𝑈𝑛𝑐𝑙𝑒 ▪ Functions: 𝑀𝑜𝑡ℎ𝑒𝑟, 𝐹𝑎𝑡ℎ𝑒𝑟 10S3001-AI | Institut Teknologi Del 12 12 First Order Logic Kinship "One's mother is one's female parent" 𝑚, 𝑐 𝑀𝑜𝑡ℎ𝑒𝑟(𝑐) = 𝑚  𝐹𝑒𝑚𝑎𝑙𝑒(𝑚) ∧ 𝑃𝑎𝑟𝑒𝑛𝑡(𝑚, 𝑐) "A sibling is another female parent" 𝑥, 𝑦 𝑆𝑖𝑏𝑙𝑖𝑛𝑔(𝑥, 𝑦)  𝑥  𝑦 ∧ 𝑝 𝑃𝑎𝑟𝑒𝑛𝑡(𝑝, 𝑥) ∧ 𝑃𝑎𝑟𝑒𝑛𝑡(𝑝, 𝑦) "Wendy is female" 𝐹𝑒𝑚𝑎𝑙𝑒(𝑤𝑒𝑛𝑑𝑦) These are axioms 10S3001-AI | Institut Teknologi Del 13 13 First Order Logic Wumpus: Time domain included Can be represented more concisely ▪ at time step 3: 𝑃𝑒𝑟𝑐𝑒𝑝𝑡([𝑆𝑡𝑒𝑛𝑐ℎ, 𝐵𝑟𝑒𝑒𝑧𝑒, 𝐺𝑙𝑖𝑡𝑡𝑒𝑟, 𝑁𝑜𝑛𝑒, 𝑁𝑜𝑛𝑒], 3) ▪ at time step 6: 𝑃𝑒𝑟𝑐𝑒𝑝𝑡([𝑁𝑜𝑛𝑒, 𝐵𝑟𝑒𝑒𝑧𝑒, 𝑁𝑜𝑛𝑒, 𝑁𝑜𝑛𝑒, 𝑆𝑐𝑟𝑒𝑎𝑚], 6) ▪ Actions can be: 𝑇𝑢𝑟𝑛(𝑅𝑖𝑔ℎ𝑡), 𝑇𝑢𝑟𝑛(𝐿𝑒𝑓𝑡), 𝐹𝑜𝑟𝑤𝑎𝑟𝑑, 𝑆ℎ𝑜𝑜𝑡, 𝐺𝑟𝑎𝑏, 𝐶𝑙𝑖𝑚𝑏 And we can 𝐴𝑆𝐾 the best action at time step 5 𝐴𝑆𝐾𝑉𝐴𝑅𝑆(𝑎 𝐵𝑒𝑠𝑡𝐴𝑐𝑡𝑖𝑜𝑛(𝑎, 5)) 10S3001-AI | Institut Teknologi Del 14 14 FOL: Wumpus Encoding complex rules Can encode ▪ Raw percepts: 𝑡, 𝑠, 𝑔, 𝑚, 𝑐, 𝑃𝑒𝑟𝑐𝑒𝑝𝑡([𝑠, 𝑏, 𝐺𝑙𝑖𝑡𝑡𝑒𝑟, 𝑚, 𝑐], 𝑡)  𝐺𝑙𝑖𝑡𝑡𝑒𝑟(𝑡) ▪ Reflex actions: 𝑡 𝐺𝑙𝑖𝑡𝑡𝑒𝑟(𝑡)  𝐵𝑒𝑠𝑡𝐴𝑐𝑡𝑖𝑜𝑛(𝐺𝑟𝑎𝑏, 𝑡) Instead of encoding stuff like: 𝐴𝑑𝑗𝑎𝑐𝑒𝑛𝑡(𝑆𝑞𝑢𝑎𝑟𝑒1,2, 𝑆𝑞𝑢𝑎𝑟𝑒1,1) 𝐴𝑑𝑗𝑎𝑐𝑒𝑛𝑡(𝑆𝑞𝑢𝑎𝑟𝑒3,4, 𝑆𝑞𝑢𝑎𝑟𝑒4,4) Encode: 𝑥, 𝑦, 𝑎, 𝑏 𝐴𝑑𝑗𝑎𝑐𝑒𝑛𝑡 𝑥, 𝑦 , 𝑎, 𝑏  (𝑥 = 𝑎 ∧ (𝑦 = 𝑏 − 1 ∨ 𝑦 = 𝑏 + 1)) ∨ (𝑦 = 𝑏 ∧ (𝑥 = 𝑎 − 1 ∨ 𝑥 = 𝑎 + 1)) 10S3001-AI | Institut Teknologi Del 15 15 First Order Logic Legos ▪ Define pieces: 𝐿𝑜𝑛𝑔(𝑝), 𝑆ℎ𝑜𝑟𝑡(𝑝), etc. ▪ and restriction: 𝑝 𝐿𝑜𝑛𝑔(𝑝)  ¬(𝐿𝑜𝑛𝑔(𝑝) ∧ 𝑆ℎ𝑜𝑟𝑡(𝑝)) ▪ Define rules: ▪ 𝑥, 𝑦, 𝑧 𝐶𝑎𝑛𝐶𝑜𝑛𝑛𝑒𝑐𝑡𝑊𝑖𝑡ℎ𝑂𝑣𝑒𝑟𝑙𝑎𝑝(𝑥, 𝑦, 𝑧)  𝑥  𝑦 ∧ 𝑃𝑖𝑒𝑐𝑒(𝑥) ∧ 𝑃𝑖𝑒𝑐𝑒(𝑦) ∧ 𝑁𝑢𝑚𝑏𝑒𝑟(𝑧) ∧ 𝑉𝑎𝑙𝑢𝑒(𝑧) ≤ 𝑂𝑣𝑒𝑟𝑙𝑎𝑝(𝑥, 𝑦) … ▪ 𝑥, 𝑦 𝑆ℎ𝑜𝑟𝑡(𝑥) ∧ 𝑆ℎ𝑜𝑟𝑡(𝑦) ∧ 𝑂𝑣𝑒𝑟𝑙𝑎𝑝(𝑥, 𝑦)  1  𝑊𝑒𝑎𝑘𝐿𝑖𝑛𝑘(𝑥, 𝑦) 10S3001-AI | Institut Teknologi Del 16 16 Creating a Knowledge Base ▪ Identify the Task ▪ Assemble the relevant knowledge ▪ Decide on a vocabulary of predicates, functions, and constants ▪ Encode general knowledge about the domain (rules) ▪ Encode a description of the problem ▪ Pose queries to the inference procedure and get answers ▪ Debug the KB 10S3001-AI | Institut Teknologi Del 17 17 Inference in First Order Logic Given 𝑥 𝐾𝑖𝑛𝑔(𝑥) ∧ 𝐺𝑟𝑒𝑒𝑑𝑦(𝑥)  𝐸𝑣𝑖𝑙(𝑥) We can infer: ▪ 𝐾𝑖𝑛𝑔(𝐽𝑜ℎ𝑛) ∧ 𝐺𝑟𝑒𝑒𝑑𝑦(𝐽𝑜ℎ𝑛)  𝐸𝑣𝑖𝑙(𝐽𝑜ℎ𝑛) ▪ 𝐾𝑖𝑛𝑔(𝑅𝑖𝑐ℎ𝑎𝑟𝑑) ∧ 𝐺𝑟𝑒𝑒𝑑𝑦(𝑅𝑖𝑐ℎ𝑎𝑟𝑑)  𝐸𝑣𝑖𝑙(𝑅𝑖𝑐ℎ𝑎𝑟𝑑) ▪ 𝐾𝑖𝑛𝑔(𝐹𝑎𝑡ℎ𝑒𝑟(𝐽𝑜ℎ𝑛)) ∧ 𝐺𝑟𝑒𝑒𝑑𝑦(𝐹𝑎𝑡ℎ𝑒𝑟(𝐽𝑜ℎ𝑛))  𝐸𝑣𝑖𝑙(𝐹𝑎𝑡ℎ𝑒𝑟(𝐽𝑜ℎ𝑛)) 10S3001-AI | Institut Teknologi Del 18 18 Inference in First Order Logic ▪ Universal Instantiation (in a  rule, substitute all symbols) ▪ Existential Instantiation (in a  rule, substitute one symbol, use the rule and discard) ▪ Skolem Constants is a new variable that represents a new inference. 10S3001-AI | Institut Teknologi Del 19 19 Inference in First Order Logic Suppose KB: ▪ 𝑥 𝐾𝑖𝑛𝑔(𝑥) ∧ 𝐺𝑟𝑒𝑒𝑑𝑦(𝑥)  𝐸𝑣𝑖𝑙(𝑥) ▪ 𝐾𝑖𝑛𝑔(𝐽𝑜ℎ𝑛) ▪ 𝐺𝑟𝑒𝑒𝑑𝑦(𝑥) ▪ 𝐵𝑟𝑜𝑡ℎ𝑒𝑟(𝑅𝑖𝑐ℎ𝑎𝑟𝑑, 𝐽𝑜ℎ𝑛) Apply Universal Instantiation using {𝑥/𝐽𝑜ℎ𝑛} and {𝑥/𝑅𝑖𝑐ℎ𝑎𝑟𝑑} ▪ 𝐾𝑖𝑛𝑔(𝐽𝑜ℎ𝑛) ∧ 𝐺𝑟𝑒𝑒𝑑𝑦(𝐽𝑜ℎ𝑛)  𝐸𝑣𝑖𝑙(𝐽𝑜ℎ𝑛) ▪ 𝐾𝑖𝑛𝑔(𝑅𝑖𝑐ℎ𝑎𝑟𝑑) ∧ 𝐺𝑟𝑒𝑒𝑑𝑦(𝑅𝑖𝑐ℎ𝑎𝑟𝑑)  𝐸𝑣𝑖𝑙(𝑅𝑖𝑐ℎ𝑎𝑟𝑑) And discard the Universally quantified sentence. We can get the KB to be propositions. 10S3001-AI | Institut Teknologi Del 20 20 Inference in First Order Logic Suppose KB: ▪ 𝑥 𝐾𝑖𝑛𝑔(𝑥) ∧ 𝐺𝑟𝑒𝑒𝑑𝑦(𝑥)  𝐸𝑣𝑖𝑙(𝑥) ▪ 𝐾𝑖𝑛𝑔(𝐽𝑜ℎ𝑛) ▪ 𝑦 𝐺𝑟𝑒𝑒𝑑𝑦(𝑦) Apply Universal Instantiation using {𝑥/𝐽𝑜ℎ𝑛} and {𝑦/𝐽𝑜ℎ𝑛} 10S3001-AI | Institut Teknologi Del 21 21 Inference Generalized Modus Ponens for atomic sentences 𝑝𝑖, 𝑝𝑖′ , and 𝑞, where there is a substitution  such that 𝑆𝑈𝐵𝑆𝑇 𝜃, 𝑝𝑖′ = 𝑆𝑈𝐵𝑆𝑇 𝜃, 𝑝𝑖 , for all 𝑖 𝑝1′ , 𝑝2′ , … , 𝑝𝑛′ , 𝑝1 ∧ 𝑝2 ∧ ⋯ ∧ 𝑃𝑛 ⇒ 𝑞 𝑆𝑈𝐵𝑆𝑇 𝜃, 𝑞 𝑝1′ = 𝐾𝑖𝑛𝑔 𝐽𝑜ℎ𝑛 𝑝1 = 𝐾𝑖𝑛𝑔 𝑥 𝑝2′ = 𝐺𝑟𝑒𝑒𝑑𝑦 𝑦 𝑝2 = 𝐺𝑟𝑒𝑒𝑑𝑦 𝑥 𝜃 = 𝑥Τ𝐽𝑜ℎ𝑛 , 𝑦Τ𝐽𝑜ℎ𝑛 𝑞 = 𝐸𝑣𝑖𝑙 𝑥 𝑆𝑈𝐵𝑆𝑇 𝜃, 𝑞 10S3001-AI | Institut Teknologi Del 22 22 Inference Unification 𝑈𝑁𝐼𝐹𝑌 𝑝, 𝑞 = 𝜃 where 𝑆𝑈𝐵𝑆𝑇 𝜃, 𝑝 = 𝑆𝑈𝐵𝑆𝑇 𝜃, 𝑞 For example: ▪ We ask 𝐴𝑆𝐾𝑉𝐴𝑅𝑆 𝐾𝑛𝑜𝑤𝑠 𝐽𝑜ℎ𝑛, 𝑥 (whom does John know?) ▪ 𝑈𝑁𝐼𝐹𝑌 𝐾𝑛𝑜𝑤𝑠 𝐽𝑜ℎ𝑛, 𝑥 , 𝐾𝑛𝑜𝑤𝑠 𝐽𝑜ℎ𝑛, 𝐽𝑎𝑛𝑒 = 𝑥Τ𝐽𝑎𝑛𝑒 ▪ 𝑈𝑁𝐼𝐹𝑌 𝐾𝑛𝑜𝑤𝑠 𝐽𝑜ℎ𝑛, 𝑥 , 𝐾𝑛𝑜𝑤𝑠 𝑦, 𝐵𝑖𝑙𝑙 = 𝑦Τ𝐽𝑜ℎ𝑛 , 𝑥Τ𝐵𝑖𝑙𝑙 ▪ 𝑈𝑁𝐼𝐹𝑌 𝐾𝑛𝑜𝑤𝑠 𝐽𝑜ℎ𝑛, 𝑥 , 𝐾𝑛𝑜𝑤𝑠 𝑦, 𝑀𝑜𝑡ℎ𝑒𝑟 𝑦 = 𝑦Τ𝐽𝑜ℎ𝑛 , 𝑥Τ𝑀𝑜𝑡ℎ𝑒𝑟 𝐽𝑜ℎ𝑛 Algorithm in the book (goes variable by variable recursively unifying) 10S3001-AI | Institut Teknologi Del 23 23 Inference Putting it all together "The Law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, and enemy of America, has some missiles , and all of its missiles were sold to it by Colonel West, who is American" Prove that Colonel Wes is a Criminal 10S3001-AI | Institut Teknologi Del 24 24 Inference The KB "The Law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, and enemy of America, has some missiles , and all of its missiles were sold to it by Colonel West, who is American" ▪ R1: 𝐴𝑚𝑒𝑟𝑖𝑐𝑎𝑛 𝑥 ∧ 𝑊𝑒𝑎𝑝𝑜𝑛 𝑦 ∧ 𝑆𝑒𝑙𝑙𝑠(𝑥, 𝑦. 𝑧) ∧ 𝐻𝑜𝑠𝑡𝑖𝑙𝑒 𝑧 ⇒ 𝐶𝑟𝑖𝑚𝑖𝑛𝑎𝑙 𝑥 ▪ R2: 𝑂𝑤𝑛𝑠(𝑁𝑜𝑛𝑜; 𝑀1 ) Nono has some missiles ▪ R3: 𝑀𝑖𝑠𝑠𝑖𝑙𝑒(𝑀1 ) ▪ R4: 𝑀𝑖𝑠𝑠𝑖𝑙𝑒 𝑥 ⇒ 𝑊𝑒𝑎𝑝𝑜𝑛 𝑥 A missile is a weapon ▪ R5: 𝑀𝑖𝑠𝑠𝑖𝑙𝑒 𝑥 ∧ 𝑂𝑤𝑛𝑠 𝑁𝑜𝑛𝑜, 𝑥 ⇒ 𝑆𝑒𝑙𝑙𝑠 𝑊𝑒𝑠𝑡, 𝑥, 𝑁𝑜𝑛𝑜 All missiles sold by west ▪ R6: 𝐸𝑛𝑒𝑚𝑦 𝑥, 𝐴𝑚𝑒𝑟𝑖𝑐𝑎 ⇒ 𝐻𝑜𝑠𝑡𝑖𝑙𝑒 𝑥 Enemies of America are hostile ▪ R7: 𝐴𝑚𝑒𝑟𝑖𝑐𝑎𝑛 𝑊𝑒𝑠𝑡 West is american ▪ R8: 𝐸𝑛𝑒𝑚𝑦 𝑁𝑜𝑛𝑜, 𝐴𝑚𝑒𝑟𝑖𝑐𝑎 10S3001-AI | Institut Teknologi Del 25 25 Inference Graph 10S3001-AI | Institut Teknologi Del 26 26 Forward Chaining ASK Iterations Iteration 1: ▪ R5 satisfied with 𝑥/𝑀1 and R9: 𝑆𝑒𝑙𝑙𝑠(𝑊𝑒𝑠𝑡, 𝑀1 , 𝑁𝑜𝑛𝑜) is added ▪ R4 satisfied with 𝑥/𝑀1 and R10: 𝑊𝑒𝑎𝑝𝑜𝑛(𝑀1 ) is added ▪ R6 satisfied with 𝑥/𝑁𝑜𝑛𝑜 and R11: 𝐻𝑜𝑠𝑡𝑖𝑙𝑒(𝑁𝑜𝑛𝑜) is added Iteration 2: ▪ R1 is satisfied with 𝑥 Τ𝑊𝑒𝑠𝑡 , 𝑦Τ𝑀1 , 𝑧Τ𝑁𝑜𝑛𝑜 and 𝐶𝑟𝑖𝑚𝑖𝑛𝑎𝑙(𝑊𝑒𝑠𝑡) is added. 10S3001-AI | Institut Teknologi Del 27 27 Inference in First Order Logic Discussion ▪ Once we have facts that evaluate to T (True) or F (False) ▪ We can apply Forward Chaining, Backwards Chaining and Resolution ▪ The key is to understand Unification ▪ Very similar to propositional logic 10S3001-AI | Institut Teknologi Del 28 28 References ▪ S. J. Russell and P. Borvig, Artificial Intelligence: A Modern Approach (4th Edition), Prentice Hall International, 2020. 10S3001-AI | Institut Teknologi Del 29 29  eof 10S3001-AI | Institut Teknologi Del 30 30