First order logic exercise set PDF

Preview

Summary

Download First order logic exercise set PDF

Description

FIRST ORDER LOGIC EXERCISE SET Exercise 1 (use of quantifiers): Translate these sentences from natural language to the language of first order logic. Use the predicate Loves, where Loves(x,y) means “x loves y”. a) “There is someone who loves everyone”. b) “There is someone who loves at least one person”. c) “There is someone who loves someone else”. d) “Everybody loves each other”. e) “There is someone who is loved by everyone”. f) “There is someone whom everybody loves”. g) “Everyone has someone who loves him (or her)”. Exercise 2 (ontology of lists): Consider the following ontology for lists: –The function Insert(x,y) inserts the element x at the beginning of the list y. For example, the list (A, B, C) is modeled by this term: Insert(A, Insert(B, Insert(C, EmptyList))) where EmptyList is a constant symbol which stands for the empty list. –The function Last(x) returns the last element of a nonempty list. It returns the constant ListError for an empty list. –The axioms of the ontology are as follows: i) The empty list has no last element. ii) The last element of a list with a single element is that element. iii) The last element of a list y is also the last element of any list constructed by inserting an element at the beginning of y. –Your task is to translate the axioms of the ontology to the language of first order logic, and then explain how to find the last element of the list (A, B, C, D) with the help of a theorem prover. Exercise 3 (Peano axioms) The Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. They have been used nearly unchanged until now. Here your task is to translate a subset of them and the definition of the sum to the language of first order logic. Then explain how to show that sum is commutative with the help of a theorem prover. Finally, explain how to find out the result of the sum 2+3 with a theorem prover. i) 0 is a natural number. ii) For every natural number n, its successor Suc(n) is also a natural number. iii) For every natural number n, Suc(n) = 0 is false. That is, there is no natural number whose successor is 0. iv) For all natural numbers m and n, if Suc(m)=Suc(n), then m=n. That is, Suc is an injection. v) The sum is defined by the following equations: a+0=a; a+Suc(b)=Suc(a+b). Exercise 4 (vector spaces): A vector space over a field F is a set V together with two binary operations that satisfy the eight axioms listed below. Here your first task is to translate these axioms

into the language of first order logic. Then explain how to show that the following property holds with the help of a theorem prover: (−v) + (−w) = –(v+w). i) Associativity of addition: u + (v + w) = (u + v) + w ii) Commutativity of addition: u + v = v + u iii) Identity element of addition: There exists an element 0  V, called the zero vector, such that v + 0 = v for all v  V. iv) Inverse elements of addition: For every v  V, there exists an element −v  V, called the additive inverse of v, such that v + (−v) = 0 . v) Distributivity of scalar multiplication with respect to vector addition: a(u + v) = au + av . vi) Distributivity of scalar multiplication with respect to field addition: (a + b)v = av + bv . vii) Compatibility of scalar multiplication with field multiplication: a(bv) = (ab)v . viii) Identity element of scalar multiplication 1v = v, where 1 denotes the multiplicative identity in F. Exercise 5 (barber’s paradox): Translate the assertions below as sentences of first order logic. This is the barber’s paradox by Bertrand Russell; it turns out that that the two of them cannot be true together in any interpretation. How would you prove this with the help of a theorem prover? i) Anyone who does not shave himself must be shaved by the barber (please note that there is only one barber). ii) Whomever the barber shaves, must not shave himself. Exercise 6 (reading first order sentences): Translate into English the following sentences of first order logic and determine which of them represent true assertions when interpreted in the set of real numbers, R. a) x x 0 b)  x x = x 2  x < 0 c) x y x > y  y > x d) x y x > y  x > y2 e) x y x + y = x f) x y x + y = y g) x y x > y  –x > y h) xy x > y  (x > y) i) xy y > x  y2 > x j) xy x > y  x > y2 k) x y z xy = yz l) x y z (x + y)z = 1 m) x y x > y  z (x > z  z > y) n) x z y x > z  z > y Exercise 7 (formalization): Translate the following arguments to the language of first order logic. They come from Lewis Carroll’s book Symbolic Logic: a) All lions are fierce. Some lions do not drink coffee.

Some fierce creatures do not drink coffee. b) No professors are ignorant. All ignorant people are vain. No professors are vain. c) Babies are illogical. Nobody is despised who can manage a crocodile. Illogical persons are despised. Babies cannot manage crocodiles. Exercise 8: Translate this argument from natural language to the language of first order logic: All dogs like meat. Dogs eat everything they like. Stubby is a dog. Therefore, Stubby eats meat. Exercise 9: Translate the following argument from natural language to the language of first order logic: One of the pupils studies Pupils study and go to the library There are no footballers in the library Juan is a footballer _____________________________________ Juan does not study

Exercise 10 (formalization and first order resolution): Write the following argument in the language of first order logic. You must model it in the form KB |= . Then establish the validity of the argument by the resolution algorithm or give a counterexample to show that it is invalid. 1. 2. 3. 4. 5.

All hounds howl at night. Anyone who has any cats will not have any mice. Light sleepers do not have anything which howls at night. John has either a cat or a hound. (Conclusion) If John is a light sleeper, then John does not have any mice.

Exercise 11: Translate this argument from natural language to the language of first order logic:

If an inspector suspects someone of theft, then he/she is questioned. Clouseau is an inspector. Lupin is not questioned. Therefore, Clouseau does not suspect Lupin of theft. Exercise 12: Translate the following argument from natural language to the language of first order logic: All students passed History or Biology. Manuel is a student. Manuel did not pass Biology. _____________________________________ At least one student passed History.

POSSIBLE SOLUTIONS Exercise 1 (use of quantifiers): a) x y Loves(x,y) b) x y Loves(x,y) c) x y Loves(x,y)  xy d) x y Loves(x,y) e) x y Loves(y,x) f) x y Loves(y,x) g) x y Loves(y,x) Exercise 2 (ontology of lists): The axioms of the ontology are expressed in first order logic as follows: i) Last(EmptyList)=ListError ii) x Last(Insert(x,EmptyList))=x iii) x y yEmptyList  Last(Insert(x,y))=Last(y) The last element of the list (A, B, C, D) can be found with the help of a theorem prover by considering i) – iii) as a KB, and then asking the following to the prover: ASKVARS(KB, x=Last(Insert(A, Insert(B, Insert(C, Insert(D, EmptyList)))))) The output of the prover should be that the above formula is entailed by the KB with the binding list {x/D}, which indicates that constant D is the last element of the list. Exercise 3 (Peano axioms) The axioms and definitions are translated to the language of first order logic as follows: i) This means that we need a constant Zero. No sentence of first order logic is necessary. ii) This means that we need a function Suc. No sentence of first order logic is necessary. iii) n Suc(n)  0 iv) m n Suc(m)=Suc(n)  m=n v) [ a Sum(a,Zero)=a ]  [ a b Sum(a,Suc(b))=Suc(Sum(a,b)) ] To show that sum is commutative with the help of a theorem prover, we consider iii)-v) as the KB, and then we ask the theorem prover whether the first order logic sentence for the commutativity of the sum is valid: ASK( KB, a b Sum(a,b)=Sum(b,a) ) The result of the sum 2+3 can be found by asking the following to the prover: ASKVARS( KB, x=Sum(Suc(Suc(Zero)), Suc(Suc(Suc(Zero)))) ) The output of the prover should be that the above formula is entailed by the KB with the binding list { x / Suc(Suc(Suc(Suc(Suc(Zero))))) }, which indicates that 2+3=5. Exercise 4 (vector spaces): The axioms are translated to the language of first order logic as follows: i) u v w Vector(u)  Vector(v)  Vector(w)  Sum(u,Sum(v,w))=Sum(Sum(u,v),w) ii) u v Vector(u)  Vector(v)  Sum(u,v)=Sum(v,u)

iii) v Vector(v)  Sum(v,ZeroVector)=v iv) v Vector(v)  Sum(v,Inverse(v))=ZeroVector v) u v a Vector(u)  Vector(v)  Scalar(a)  Product(a,Sum(u,v))=Sum(Product(a,u),Product(a,v)) vi) v a b Vector(v)  Scalar(a)  Scalar(b)  Product(FieldSum(a,b),v)=Sum(Product(a,v),Product(b,v)) vii) v a b Vector(v)  Scalar(a)  Scalar(b)  Product(a,Product(b,v))=Product(FieldProduct(a,b),v) viii) v Vector(v)  Product(ScalarOne,v)=v To show that (−v) + (−w) = –(v+w), we consider i)-viii) as the KB, and then we ask the theorem prover whether the first order logic sentence for the desired property is valid: ASK( KB, v w Vector(v)  Vector(w)  Sum(Inverse(v),Inverse(w))=Inverse(Sum(v,w)) ) Exercise 5 (barber’s paradox): The assertions are expressed in first order logic as follows: i) x Shaves(x, x)  Shaves(Barber, x) ii) x Shaves(Barber, x)  Shaves(x, x)) To show that both conditions can not hold at the same time, we use an empty KB and then we ask the theorem prover whether the negation of the conjunction of both conditions is valid (and the answer should be ‘yes’): ASK( KB, ( [x Shaves(x, x)  Shaves(Barber, x) ]  [ x Shaves(Barber, x)  Shaves(x, x)) ] ) ) Exercise 6 (reading first order sentences): a) Not every real number is different from 0. True. b) There exists a real number which, if that number equals its square, then it is negative. True: take any x such that x  x2. Then the antecedent is false so the implication is true. c) For every pair of real numbers x and y, one of them is less than the other. False: take x = y. d) For every real x there is a real y such that if x is greater than y then it is also greater than the square of y. True: given x take y = x. e) There is a real number x which can be added to any real number y to obtain again x. False. f) There is a real number x which can be added to any real number y to obtain again y. True: take x = 0. g) There is a real number x such that, for every real number y, x is greater than y or –x is greater than y. False. h) There is a real number x such that for every real number y, either x is greater than y or it is not. True: law of excluded middle. i) There is a real x such that every real y greater than x will have a square also greater than x. True: take e.g. x = 1. j) There is a real x such that every real y less than x will have a square also less than x. False.

k) For any real number x, there is some real number y so that xy will equal yz for all real numbers z. True: given x, take y = 0. l) There is a real number x such that, given any real number y, (x + y)z equals 1 for some real number z. False: given x, take y = –x. m) Between any two distinct real numbers there lies another real number. True: density of R. n) Given any real number x, there is some real number z so that if x is greater than z then z will be greater than every real number. True: given x, take z = x. Exercise 7 (formalization): a) x Lion(x)  Fierce(x) x Lion(x)  Drinks(x,Coffee) x Fierce(x)  Drinks(x,Coffee) b)  [ x Professor(x)  Ignorant(x) ] x Ignorant(x)  Vain(x)  [ x Professor(x)  Vain(x) ] c) x Baby(x)  Illogical(x) x [ y Crocodile(y)  Manages(x,y) ]  Despised(x) x Illogical(x)  Despised(x) x Baby(x)   [ y Crocodile(y)  Manages(x,y) ] Exercise 8: x Dog(x)  Likes(x,Meat) x,y Dog(x)  Likes(x,y)  Eats(x,y) Dog(Stubby) |= Eats(Stubby,Meat) Exercise 9: x [Pupil(x)  Studies(x)] x [Pupil(x) → Studies(x)  Library(x)] ||| a possible alternative: x [Pupil(x) → Studies(x)  Goes(x, Library)] x [Library(x)  Footballer(x)] ||| a possible alternative: x [Library(x) →Footballer(x)] Footballer(Juan) __________________________________________________________________ Studies(Juan)

Exercise 10 (formalization and first order resolution): A possible formalization of the given facts is shown below, where LS(x) stands for 'x is a light sleeper'. 1. 2. 3. 4. 5.

 x (Hound(x)  Howl(x))  x,y (Have (x,y)  Cat (y)  ¬  z (Have(x,z)  Mouse (z)))  x (LS(x)  ¬  y (Have (x,y)  Howl(y)))  x (Have (John,x)  (Cat(x)  Hound(x))) LS(John)  ¬  z (Have(John,z)  Mouse(z)) The next step is to transform each formula into conjunctive normal form:

1.  x (Hound(x)  Howl(x)) ¬ Hound(x)  Howl(x) 2.  x, y (Have (x,y)  Cat (y)  ¬  z (Have(x,z)  Mouse (z))) ¬ Have(x,y)  ¬ Cat(y)  ¬ Have(x,z)  ¬ Mouse(z) 3.  x (LS(x)  ¬  y (Have (x,y)  Howl(y))) ¬ LS(x)  ¬ Have(x,y)  ¬ Howl(y) 4.  x (Have (John,x)  (Cat(x)  Hound(x))) Have(John,a)  (Cat(a)  Hound(a)) where a is a Skolem constant. 5. ¬ [LS(John)  ¬  z (Have(John,z)  Mouse(z))] (negated conclusion) LS(John)  Have(John,b)  Mouse(b) where b is another Skolem constant. The set of clauses for this problem is thus as follows: 1. ¬ Hound(x)  Howl(x) 2. ¬ Have(x,y)  ¬ Cat(y)  ¬ Have(x,z)  ¬ Mouse(z) 3. ¬ LS(x)  ¬ Have(x,y)  ¬ Howl(y) 4. a. Have(John,a) b. Cat(a)  Hound(a) 5. a. LS(John) b. Have(John,b) c. Mouse(b)

Now we proceed to prove the conclusion by resolution using the above clauses. Each result clause is numbered; the numbers of its parent clauses are shown to its left. [1.,4.b:] 6. Cat(a)  Howl(a) [2,5.c:] 7. ¬ Have(x,y)  ¬ Cat(y)  ¬ Have(x,b) [7,5.b:] 8. ¬ Have(John,y)  ¬ Cat(y) [6,8:] 9. ¬ Have(John,a)  Howl(a) [4.a,9:] 10. Howl(a) [3,10:] 11. ¬ LS(x)  ¬ Have(x,a) [4.a,11:] 12. ¬ LS(John) [5.a,12:] 13. False Exercise 11: x,y Inspector(x)  Suspects(x,y)  Questioned(y) Inspector(Clouseau) Questioned(y) |= Suspects(Clouseau,Lupin) Exercise 12: x Student(x)  (Passed(x, History)  Passed(x, Biology) ) Student(Manuel)  Passed(Manuel, Biology) _____________________________________ x Student(x)  Passed(x, History)...