/*@ @*/ // ============================================================== // // firstOrderSemantics.txt // An demonstration exercise in first order logic (semantics). // (c) 2018, Project LogTechEdu, http://fmv.jku.at/logtechedu/ // // This exercise consists of 5 tasks TASK 1-5 where each task // consists of one ore more questions a,b,... // // This file is for demonstration; it provides both the questions // and corect answers to these questions. Study the questions, its // answers, and run the checks of the correctness of the answers. // // ============================================================== /*@ ----------------------------- TASK 1 DESCRIPTION: ----------------------------- Below you see the definition @*/ //@ pred p1(x:ℕ[3], y:ℕ[3]) ⇔ x > 0 ∧ y+1 = x ; //@ /*@ of a predicate p1(x,y) by a formula F with two free variables x,y; these variables (and all variables bound in F) may be assigned values from the domain ℕ[3] = { 0,1,2,3 }. TASK 1.a: Give all satisfying assignments of p1(x,y) by a comma-separated list << x-value , y-value >> , ... of all pairs of values from ℕ[3] that when assigned to x,y make p1(x,y) true: @*/ val a1 = {//@ << 1 , 0 >> , << 2 , 1 >> , << 3 , 2 >> //@ } ; theorem ass1() ⇔ a1 = { ⟨x,y⟩ | x:ℕ[3], y:ℕ[3] with p1(x,y) }; fun num1():ℕ[16] = |{ ⟨x,y⟩ | x:ℕ[3], y:ℕ[3] with p1(x,y) }|; /*@ Check the correctness of your answer: @*/ /*@ @*/ /*@ If your answer is not correct, see here the number of satisfying assignments: @*/ /*@ @*/ /*@ If your answer is still not correct, see here the satisfying assignments: @*/ /*@ @*/ /*@ TASK 1.b: The formula p1(x,y) is satisfiable. True? (enter "true" or "false") @*/ theorem sat1() ⇔ /*@@*/true/*@@*/ ⇔ ∃x:ℕ[3],y:ℕ[3]. p1(x,y); /*@ @*/ /*@ TASK 1.c: The formula p1(x,y) is valid. True? (enter "true" or "false") @*/ //@ theorem valid1() ⇔ /*@@*/false/*@@*/ ⇔ ∀x:ℕ[3],y:ℕ[3]. p1(x,y); /*@ @*/ /*@ ----------------------------- TASK 2 DESCRIPTION: ----------------------------- Below you see the definition @*/ //@ pred p2(x:ℕ[3]) ⇔ ∃y:ℕ[3]. y+1 = x ; //@ /*@ of a predicate p2(x) by a formula F with one free variable x; this variable (and all variables bound in F) may be assigned values from the domain ℕ[3] = { 0,1,2,3 }. TASK 2.a: Give all satisfying assignments of p2(x) by a comma-separated list x-value , ... of all values from ℕ[3] that when assigned to x make p2(x) true. @*/ val a2 = {//@ 1, 2, 3 //@ } ; //@ theorem ass2() ⇔ a2 = { x | x:ℕ[3] with p2(x) }; fun num2():ℕ[4] = |{ x | x:ℕ[3] with p2(x) }|; /*@ Check the correctness of your answer: @*/ /*@ @*/ /*@ If your answer is not correct, see here the number of satisfying assignments: @*/ /*@ @*/ /*@ If your answer is still not correct, see here the satisfying assignments: @*/ /*@ @*/ /*@ TASK 2.b: The formula p2(x) is satisfiable. True? (enter "true" or "false") @*/ theorem sat2() ⇔ /*@@*/true/*@@*/ ⇔ ∃x:ℕ[3],y:ℕ[3]. p1(x,y); /*@ @*/ /*@ TASK 2.c: The formula p2(x) is valid. True? (enter "true" or "false") @*/ //@ theorem valid2() ⇔ /*@@*/false/*@@*/ ⇔ ∀x:ℕ[3],y:ℕ[3]. p1(x,y); /*@ @*/ /*@ ----------------------------- TASK 3 DESCRIPTION: ----------------------------- Below you see the definition @*/ //@ pred p3() ⇔ ∃y:ℕ[3]. ∀x:ℕ[3]. x > 0 ⇒ ∃y:ℕ[3]. y+1 = x ; //@ /*@ of a predicate p3() by a closed formula F. Give the truth value of p3() (enter "true" or "false"): @*/ theorem valid3() ⇔ p3() ⇔ /*@@*/true/*@@*/; /*@ @*/ /*@ ----------------------------- TASK 4 DESCRIPTION: ----------------------------- In the following we consider formulas interpreted over the domain ℕ[2] = { 0,1,2 }. Below you see two definitions @*/ type Formula1 = Map[ℕ[2],Bool]; //@ pred a4(p:Formula1, q:Formula1) ⇔ (∃x:ℕ[2]. p[x]) ∧ (∃x:ℕ[2]. q[x]) ; pred b4(p:Formula1, q:Formula1) ⇔ ∃x:ℕ[2]. p[x] ∧ q[x] ; //@ fun implies4a(): Set[Tuple[Formula1,Formula1]] = { ⟨p,q⟩ | p:Formula1, q:Formula1 with ¬(a4(p,q) ⇒ b4(p,q)) }; /*@ with formulas in which predicates p[x] and q[x] occur; please note that applications of these predicates have to be written with square brackets [ ]. Task 4.a: F2 a logical consequence of F1. True? (enter "true" or "false") @*/ theorem task4a() ⇔ /*@@*/false/*@@*/ ⇔ (∀p:Formula1, q:Formula1. a4(p,q) ⇒ b4(p,q)); /*@ @*/ /*@ TASK 4.b: [ Only if your answer to TASK 4.a is "false". ] Give examples of two predicates p[x] and q[x] for which a4 is true and b4 is false. These examples may be simply written in the form of a two sequences p: p[0], p[1], p[2] q: q[0], q[1], q[2] of truth values that list the value of p[x] and q[x] for each value of x. @*/ fun p():Formula1 = choose p:Formula1 with p[0] = /*@@*/true/*@@*/ ∧ p[1] = /*@@*/false/*@@*/ ∧ p[2] = /*@@*/false/*@@*/ ; //@ fun q():Formula1 = choose q:Formula1 with q[0] = /*@@*/false/*@@*/ ∧ q[1] = /*@@*/true/*@@*/ ∧ q[2] = /*@@*/false/*@@*/ ; theorem task4b() ⇔ a4(p(),q()) ∧ ~b4(p(),q()); /*@ @*/ /*@ @*/ /*@ ----------------------------- TASK 5 DESCRIPTION: ----------------------------- In the following we consider formulas interpreted over the domain ℕ[2] = { 0,1,2 }. Below you see a definition @*/ type Formula2 = Map[ℕ[2],Formula1]; //@ pred a5(p:Formula1, q:Formula2) ⇔ ¬ ∀x:ℕ[2]. p[x] ⇒ ∃y:ℕ[2]. q[x][y] ; /*@ with a formula in which predicates p[x] and q[x][y] occur; please note that applications of these predicates have to be written with square brackets [ ] around every argument. Give a definition @*/ //@ pred b5(p:Formula1, q:Formula2) ⇔ /*@@*/∃x:ℕ[2]. p[x] ∧ ∀y:ℕ[2]. ¬q[x][y]/*@@*/ ; //@ /*@ with a formula that is logically equivalent to the one given above but in which the negation connective ¬ is only applied to atomic formulas (i.e., "push the negation as much inside as possible"). Note: the following will only check the equivalence of your formula to the given one, not whether your formula indeed satisfies the syntactic description given above. @*/ theorem task5() ⇔ ∀p:Formula1, q:Formula2. a5(p,q) ⇔ b5(p,q); /*@ @*/