Understanding First-Order Logic Fundamentals

Explore the limitations of propositional logic and delve into the syntax, semantics, and inference rules of first-order logic. Learn about predicates, quantification, and how to express relationships among objects using predicates. Enhance your understanding of how first-order logic provides a more expressive power compared to propositional logic.

• First-order logic
• Propositional logic
• Syntax
• Predicates
• Quantification

labi_315 Follow

Uploaded on Nov 28, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. First-order Logic Some slides are borrowed from Chelsea Finn & Nima Anari

2. Limitations of propositional logic Propositional logic is rather limited in its expressive power. E.g., For every x, x > 0 is true if x is a positive integer. We cannot say it in propositional logic. Nor can we show the following logical equivalences: "Not all birds fly" is equivalent to "Some birds don't fly". "Not all integers are even" is equivalent to "Some integers are not even". "Not all cars are expensive" is equivalent to "Some cars are not expensive . We need first-order logic. 2 CS411: Artificial Intelligence I, Bing Liu

3. Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 3 CS411: Artificial Intelligence I, Bing Liu

4. Syntax of first-order logic Terms (refer to objects): Constant symbol (e.g., Arithmetic) starts with a capital letter Variable (e.g., x) Function of terms (e.g., Sum(3, x)) Formulas: Atomic formulas (atoms): predicate applied to terms (e.g., Knows(x, Arithmetic)) Connectives applied to formulas (e.g., Student(x) Knows(x, Arithmetic)) Quantifiers applied to formulas (e.g., x Student(x) Knows(x, Arithmetic)) 4 CS411: Artificial Intelligence I, Bing Liu

5. Predicate Predicate: A predicate is a property about of some objects or a relationship among objects represented by the variables. Example "The sky is blue "The cover of this book is blue" For the above two sentences, we can use is_Blue as the predicate. We can also simply use B. B(x), where x is variable representing an arbitrary object. B(x) reads as "x is blue". 5 CS411: Artificial Intelligence I, Bing Liu

6. Another predicate example "John gives the book to Mary", "Jim gives a loaf of bread to Tom", and "Jane give a lecture to Mary" All can be expressed using this predicate: Give(x, y, z) which reads, x gives y to z. E.g., Give(John, Book, Mary), Give(Jane, Lecture, Mary) 6 CS411: Artificial Intelligence I, Bing Liu

7. Quantification A predicate with variables is not a proposition (with truth value of T or F). E.g., the statement x > 1 with variable x over the universe of real numbers is neither true nor false since we don't know what x is. It can be true or false depending on the value of x. For x > 1 to be a proposition either we substitute a specific number for x, or change it to something like "There is a number x for which x > 1 holds", or "For every number x, x > 1 holds". We are using quantifiers. 7 CS411: Artificial Intelligence I, Bing Liu

8. From predicate to propositions A predicate with variables (called an atomic formula) can be made a proposition by applying one of the following two operations to each of its variables: assign a value to the variable quantify the variable using a quantifier Let us use predicate GreatThan(x, 1) to represent x >1. universal quantifier: for every object x in the universe, x > 1 written as: x GreatThan(x, 1) existential quantifier: "for some object x in the universe, x > 1 written as: x GreatThan(x, 1) 8 CS411: Artificial Intelligence I, Bing Liu

9. Universe of Discourse The universe of discourse, also called universe (also called domain), is the set of objects of interest. Universal Quantifier ( ): The expression: x P(x), denotes the universal quantification of P(x). In English: "For all x, P(x) holds" or "for every x, P(x) holds". P(x) is true for every object x in the universe Existential Quantifier( ): The expression: xP(x), denotes the existential quantification of P(x). In English: "There exists an x such that P(x)" or "There is at least one x such that P(x) . x means at least one object x in the universe. 9 CS411: Artificial Intelligence I, Bing Liu

10. Application of Quantifiers When more than one variable is quantified in a wff such as y x P(x, y), they are applied from the inside i.e., the one closest to the atomic formula is applied first. Thus y x P(x, y), reads y [ x P(x, y)] Some properties The positions of different types of quantifiers cannot be switched. For example, x y P(x, y ) is not equivalent to y x P(x, y ). x P(x) equivalent to x P(x) 10 CS411: Artificial Intelligence I, Bing Liu

11. Examples Let P(x, y) stands for x likes y . (1). x y P(x, y): There is a person who likes every person. (2). y x P(x, y): For any person y, there is a person x who likes y. Let P(x, y) stands for x < y . (1). x y P(x, y): There is a number x that is smaller than any number y. (2). y x P(x, y): For any number, there is a smaller number 11 CS411: Artificial Intelligence I, Bing Liu

12. How to read quantified formulas Let F(x, y) stands for x flies faster than y . let the universe be the set of airplanes. x yF(x, y): "For every airplane x the following holds: x is faster than any airplane y". Or simply: "Every airplane is faster than every airplane (including itself!)". x yF(x, y): "For every airplane x the following holds: for some airplane y, x is faster than y". Or simply: "Every airplane is faster than some airplane". x y F(x, y): "There exist an airplane x which satisfies the following: (or such that) for every airplane y, x is faster than y". Or simply: some airplane is faster than every airplane". x yF(x, y): "For some airplane x there exists an airplane y such that x is faster than y . Or simply: "Some airplane is faster than some airplane". 12 CS411: Artificial Intelligence I, Bing Liu

13. Well-Formed Formula (wff) Wffs (or sentences) are constructed using the following rules: True and False are wffs. Each propositional constant (i.e., specific proposition), and each propositional variable (i.e., a variable representing propositions) are wffs. Each atomic formula (i.e. a specific predicate with variables) is a wff. If A and B are wffs, then so are A, (A B), (A B), (A B), and (A B). If x is a variable (representing objects of the universe of discourse), and A is a wff, then so are x A and x A . 13 CS411: Artificial Intelligence I, Bing Liu

14. Some examples of first-order logic There is some course that every student has taken. y Course(y) [ x Student(x) Takes(x, y)] Every even integer greater than 2 is the sum of two primes. x EvenInt(x) Greater(x, 2) y z Equals(x, Sum(y, z)) Prime(y) Prime(z) If a student takes a course and the course covers a concept, then the student knows that concept. x y z (Student(x) Takes(x, y) Course(y) Covers(y, z)) Knows(x, z) 14 CS411: Artificial Intelligence I, Bing Liu

15. Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 15 CS411: Artificial Intelligence I, Bing Liu

16. Models in first-order logic A model w in first-order logic maps: constant symbols to objects w(Alice) = o1, w(Bob) = o2, w(Arithmetic) = o3 predicate symbols to tuples of objects w(Knows) = {(o1, o3), (o2, o3), . . . } Unique names assumption: Each object has at most one constant symbol. Domain closure: Each object has at least one constant symbol. 16 CS411: Artificial Intelligence I, Bing Liu

17. Propositionalization If one-to-one mapping between constant symbols and objects: (unique names only one name for an object; domain closure at least one name), first-order logic is syntactic sugar for propositional logic E.g., Knowledge base in first-order logic Student(alice) Student(bob) x Student(x) Person(x) x Student(x) Creative(x) Knowledge base in propositional logic Studentalice Studentbob (Studentalice Personalice) (Studentbob Personbob) (Studentalice Creativealice) (Studentbob Creativebob) We can use any inference algorithm for propositional logic! 17 CS411: Artificial Intelligence I, Bing Liu

18. Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 18 CS411: Artificial Intelligence I, Bing Liu

19. Definite clauses Definite clause (first-order logic) A definite clause has the following form: x1 xn (a1 ak) b for variables x1, . . . , xn and atomic formulas a1, . . . , ak, b (which contain those variables). For example, x y z (Takes(x, y) Covers(y, z)) Knows(x, z) 19 CS411: Artificial Intelligence I, Bing Liu

20. Modus ponens (first attempt) Definition: modus ponens (first-order logic) a1, . . . , ak x1 xn(a1 ak) b b Example: Given P(Alice) and x P(x) Q(x). We cannot use the above modus ponens because P(Alice) and P(x) do not match. We need substitution and unification 20 CS411: Artificial Intelligence I, Bing Liu

21. Substitution Subst[{x/Alice}, P(x)] = P(Alice) Subst[{x/Alice, y/z}, P(x) K(x, y)] = P(Alice) K(Alice, z) Definition: Substitution A substitution is a mapping from variables to terms. Subst[ , f] returns the result of performing substitution on f. 21 CS411: Artificial Intelligence I, Bing Liu

22. Unification Unify[Knows(Alice, Arithmetic), Knows(x, Arithmetic)] = {x/Alice} Unify[Knows(Alice, y), Knows(x, z)] = {x/Alice, y/z} Unify[Knows(Alice, y),Knows(Bob, z)] = fail Unify[Knows(Alice, y),Knows(x, F(x))] = {x/Alice, y/F(Alice)} Definition: Unification Unification takes two formulas f and g and returns a substitution which is the most general unifier: Unify[f, g] = such that Subst[ , f] = Subst[ , g] or fail if no such exists. 22 CS411: Artificial Intelligence I, Bing Liu

23. Modus ponens Definition: modus ponens (first-order logic) a 1 , . . . , a k x1 xk(a1 ak) b b Get most general unifier on premises: = Unify[a 1 , . . . , a k, a1 ak] Apply to conclusion: Subst[ , b] = b 23 CS411: Artificial Intelligence I, Bing Liu

24. Modus ponens example Premises: Takes(Alice, CS411) Covers(CS411, Logic) x y z Takes(x, y) Covers(y, z) Knows(x, z) Conclusion: = {x/Alice, y/CS411, z/Logic} Derive Knows(Alice, Logic) 24 CS411: Artificial Intelligence I, Bing Liu

25. Completeness and semi-decidability Theorem: completeness Modus ponens is complete for first-order logic with only Horn clauses. Theorem: semi-decidability First-order logic (even restricted to only Horn clauses) is semi-decidable. If KB |= f, forward inference on complete inference rules will prove f in finite time. If KB |=/ f, no algorithm can show this in finite time. 25 CS411: Artificial Intelligence I, Bing Liu

26. Resolution First-order logic includes non-Horn clauses x Student(x) y Know(x, y) Resolution (same as in propositional logic): Convert all formulas to CNF (conjunctive normal form) more complex than in propositional logic. Repeatedly apply resolution rule 26 CS411: Artificial Intelligence I, Bing Liu

27. Conversion to CNF Input: Anyone who likes all animals is liked by someone Output New to first-order logic All variables (e.g., x) have universal quantifiers by default Introduce Skolem functions (e.g., Y(x)) to represent existential quantified variables. 27 CS411: Artificial Intelligence I, Bing Liu

28. Conversion to CNF (cont.) 28 CS411: Artificial Intelligence I, Bing Liu

29. Conversion to CNF (cont.) 29 CS411: Artificial Intelligence I, Bing Liu

30. Resolution of first-order logic Definition: resolution rule (first-order logic) Example 30 CS411: Artificial Intelligence I, Bing Liu

31. Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 31 CS411: Artificial Intelligence I, Bing Liu

32. Bound and free variables A variable in a wff is said to be bound if either a specific value is assigned to it or it is quantified. If an appearance of a variable is not bound, it is called free. The extent of the application (effect) of a quantifier, called the scope of the quantifier, is indicated by square brackets [ ]. If there are no square brackets, then the scope is understood to be the smallest wff following the quantification. For example, in x P(x, y), The variable x is bound while y is free. In x [ y P(x, y) Q(x, y)], x and y in P(x, y) are bound, while y in Q(x, y) is free, because the scope of y is P(x, y). The scope of x is [ y P(x, y) Q(x, y)] . 32 CS411: Artificial Intelligence I, Bing Liu

33. From Wff to Proposition A wff is, in general, not a proposition. For example, consider the wff x P(x), where P(x) means x 0. If the universe is {1, 2, 3, 4, 5, 6} or any subset of natural numbers, the wff is true. But if the universe is {-2, -3, 5}, then it is not true. Also, x Q(x, y), where Q(x, y) means x > y for the universe {1, 3, 5} may be true or false depending on the value of y. The specification of the universe and an assignment of a value to each free variable in a wff is called an interpretation for the wff. 33 CS411: Artificial Intelligence I, Bing Liu

34. Satisfiability A wff is said to be satisfiable if there exists an interpretation that makes it true, I.e., if there are a universe and an assignment of values to its free variables that make the wff true. A wff is called unsatisfiable, if there is no interpretation that makes it true. E.g.: x P(x), where P(x) means x 0, is satisfiable, if our universe is {1, 2, 3, 4, 5, 6}. x [P(x) P(x)] is not satisfiable. 34 CS411: Artificial Intelligence I, Bing Liu

35. Validity A wff is valid if it is true for every interpretation. E.g., the wff x P(x) x P(x)is valid for any predicate name P , because x P(x)is the negation of x P(x). Validity is analogue to tautology. E.g., the wff x P(x) is satisfiable but not valid. 35 CS411: Artificial Intelligence I, Bing Liu

36. Reasoning with first-order logic Predicate logic is more powerful than propositional logic as it allows one to reason about properties and relationships of individual objects. In predicate logic, one can use some additional inference rules, as well as those for propositional logic. Inference rules of predicate logic universal instantiation universal generalization existential instantiation existential generalization 36 CS411: Artificial Intelligence I, Bing Liu

37. Universal Instantiation x P(x) ---------- P(c) where c is some arbitrary element of the universe. For example, the following argument can be proven correct using the Universal Instantiation: "No humans can fly. Tom is human. Therefore, Tom cannot fly." The argument is [ x [Human(x) Fly(x)] Human(Tom) ] Fly(Tom). The proof is 1. x [Human(x) Fly(x)] 2. Human(Tom) 3. Human(Tom) Fly(Tom) 4. Fly(Tom) Hypothesis Hypothesis Universal instantiation on 1. Modus ponens on 2 and 3. 37 CS411: Artificial Intelligence I, Bing Liu

38. Universal Generalization P(c) ---------- x P(x) where P(c) holds for every element c of the universe of discourse. For every number x if x > 1, then x - 1 > 0. Also for every number x, x > 1. We conclude that for every number x, x - 1 >0. Then the argument above is represented by (P(x): x > 1; Q(x): x - 1> 0) [ x[P(x) Q(x)] x P(x)] x Q(x) To prove it we proceed as follows: 1. x [P(x) Q(x)] 2. x P(x) 3. [P(x) Q(x)] 4. P(x) for the same x as in 3. 5. Q(x) 6. x Q(x) Hypothesis Hypothesis Universal Instantiation on 1. Universal Instantiation on 2. Modus ponens on 3 and 4. Universal Generalization on 5 38 CS411: Artificial Intelligence I, Bing Liu

39. Existential Instantiation x P(x) ------- P(c) where c is some element of the universe of discourse. It is not arbitrary but must be one for which P(c) is true. If you get 95 on the final exam for CS411, then you get an A for the course. Someone, say s, gets 95 on the final exam. Therefore, s gets an A for CS411. Let the universe be the set of all people in the world, let G(x) mean that x gets 95 on the final exam of CS411, and let A(x) represent that x gets an A for CS411. Then the proof proceeds as follows: 1. x [G(x) A(x)] Hypothesis 2. x G(x) Hypothesis 3. G(s) Existential instantiation on 3. 4. G(s) A(s) Universal instantiation on 1. 5. A(s) Modus ponens on 3 and 4. 39 CS411: Artificial Intelligence I, Bing Liu

40. Existential Generalization P(c) ---------- x P(x) where c is an element of the universe. "if everyone is happy then someone is happy" To prove it, first let the universe be the set of all people and let Happy(x) mean that x is happy. Then the argument is x Happy(x) x Happy(x) The proof is 1. x Happy(x) Hypothesis 2. Happy(c) Universal instantiation 3. x Happy(x) Existential generalization. 40 CS411: Artificial Intelligence I, Bing Liu

41. Outline Syntax Semantics Inference based on modus ponens Inference based on classic reasoning Summary 41 CS411: Artificial Intelligence I, Bing Liu

42. Summary First-order logic (FOL) is a very expressive formal language as variables yield very compact knowledge representations. Many domains of technical knowledge can be written in FOL (see AIMA Ch. 10) circuits, software, planning, network and security protocols, ecommerce transactions, knowledge graph, Semantic Web, etc. Inference is semi-decidable in general; many problems are efficiently solvable in practice. 42 CS411: Artificial Intelligence I, Bing Liu