From: Amin Bandali Date: Sat, 30 Nov 2019 06:31:32 +0000 (-0500) Subject: add static se212-f19 page X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/commitdiff_plain/577bfe36d675e89cf680abcf81d12ef4fc2b750a?ds=sidebyside add static se212-f19 page --- diff --git a/haunt.scm b/haunt.scm index 5bc9039..bb6079e 100644 --- a/haunt.scm +++ b/haunt.scm @@ -366,6 +366,44 @@ "EECS 1012") ": TA in Fall 2017")))) +(define se212-f19-page + (static-page + "SE 212 Material" + "se212-f19/index.html" + `((h1 "Material from SE 212 tutorials") + (p "This page contains slides and other material from " + ,(aa "SE 212 tutorials" + "https://www.student.cs.uwaterloo.ca/~se212/times.html") + " held by me in Fall 2019. " + (del "If you have any questions, concerns, or suggestions " + "about the presented material, please email me at " + "bandali@uwaterloo.ca or come see me during my " + ,(aa "Friday office hours" + "https://www.student.cs.uwaterloo.ca/~se212/personnel.html") + ".")) + (ul + (li "Tutorial 1:" + (ul + (li ,(aa "TUT 101 slides" "se212-t01-101.pdf")) + (li ,(aa "TUT 102 slides" "se212-t01-102.pdf")) + (li ,(aa "Org beamer sources" "se212-t01.org")))) + (li "Tutorial 2:" + (ul + (li ,(aa "Homework 2 q04d solution" + "se212-h02q04d-soln.grg")))) + (li "Tutorial 3: —") + (li "Tutorial 4: —") + (li "Tutorial 5:" + (ul + (li ,(aa "Slides" "se212-t05.pdf")) + (li ,(aa "Org beamer sources" "se212-t05.org")))) + (li "Tutorial 6: —") + (li "Tutorial 7: worked through questions 1–5 of Homework 7") + (li "Tutorial 8: —") + (li "Tutorial 9: —") + (li "Tutorial 10: worked through questions 1–10 of " + "Homework 10"))))) + (site #:title "Amin Bandali" ;; TODO: uncomment after new haunt release ;; #:scheme my-scheme @@ -389,4 +427,5 @@ contact-page cv-page license-page + se212-f19-page (static-directory "static" ""))) diff --git a/se212-f19/index.html b/se212-f19/index.html deleted file mode 100644 index 4155012..0000000 --- a/se212-f19/index.html +++ /dev/null @@ -1,62 +0,0 @@ - - - - - - SE 212 Material | Amin Bandali - - - - -
-

Material from SE 212 tutorials

-

- This page contains slides and other material from - SE - 212 tutorials held by me in Fall 2019. - - If you have any questions, concerns, or suggestions about the - presented material, please email me at bandali@uwaterloo.ca or - come see me during my - Friday - office hours. -

- - -
- - - diff --git a/se212-f19/se212-h02q04d-soln.grg b/se212-f19/se212-h02q04d-soln.grg deleted file mode 100644 index e395717..0000000 --- a/se212-f19/se212-h02q04d-soln.grg +++ /dev/null @@ -1,25 +0,0 @@ -#u abandali -#a h02 - -#q q04d - -p <=> q, p & q <=> (p | q) - -#check TP - -p <=> q <-> p & q <=> (p | q) - - 1) p & q <=> (p | q) - 2) (p & q => p | q) & (p | q => p & q) by equiv - 3) (!(p & q) | p | q) & (!(p | q) | p & q) by impl * 2 - 4) (!p | !q | p | q) & (!(p | q) | p & q) by dm - 5) (true | !q | q) & (!(p | q) | p & q) by lem - 6) true & (!(p | q) | p & q) by simp1 - 7) !(p | q) | p & q by simp1 - 8) !p & !q | p & q by dm - 9) (!p & !q | p) & (!p & !q | q) by distr -10) (!p | p) & (!q | p) & (!p | q) & (!q | q) by distr * 2 -11) true & (!q | p) & (!p | q) & true by lem * 2 -12) (!q | p) & (!p | q) by simp1 * 2 -13) (q => p) & (p => q) by impl * 2 -14) p <=> q by equiv diff --git a/se212-f19/se212-t01.html b/se212-f19/se212-t01.html deleted file mode 100644 index d81cbd7..0000000 --- a/se212-f19/se212-t01.html +++ /dev/null @@ -1,343 +0,0 @@ - - - - - - - -Propositional Logic - - - - - - -
-

Propositional Logic -
-(SE 212 TUT 102) -

- -
-

1 Are you at the right place?

-
-

-We’re in MC 4040, for SE 212 TUT 102 (03:30-04:20W) -

-
-
- -
-

2

-
-
-

-George -

-
-
-
- - - -
-

4 Tool support

-
-

-Over the years, students have developed a number of tools for using -George and/or editing .grg files, such as plugins for Vim and Atom. -

- -

-Check them out at -

- -
-

-Course website → George User Manual → Contributions -

-
-
-
- -
-

5 George mode for Emacs (new!)

-
- -
-
- -
-

6 a00q01.grg (demo)

-
-

-Walk through answering a00q01.grg and submitting on MarkUs -

-
-
- -
-

7 Homework 1

-
-
    -
  • Let’s do a couple of questions from Homework 1
    • -
  • Now you try the rest, let me know if you have any questions
    • -
-
-
-
-
-

Date: Wed Sep 11, 2019

-

Author: Amin Bandali

- -

Created: 2019-09-18 Wed 23:12

-

Validate

-
- - diff --git a/se212-f19/se212-t01.org b/se212-f19/se212-t01.org deleted file mode 100644 index 12e9cdd..0000000 --- a/se212-f19/se212-t01.org +++ /dev/null @@ -1,78 +0,0 @@ -#+macro: topic Propositional Logic - -#+macro: room MC 4040 -#+macro: sec1 SE 212 TUT 101 -#+macro: sec2 SE 212 TUT 102 -#+macro: time1 02:30-03:20W -#+macro: time2 03:30-04:20W - -#+macro: sec {{{sec2}}} -#+macro: sectime {{{time2}}} - -#+title: {{{topic}}} -#+subtitle: ({{{sec}}}) -#+author: Amin Bandali -#+email: bandali@uwaterloo.ca -#+date: Wed Sep 11, 2019 -#+language: en -#+options: email:t num:t toc:nil \n:nil ::t |:t ^:t -:t f:t *:t <:t -#+options: tex:t d:nil todo:t pri:nil tags:not-in-toc -#+select_tags: export -#+exclude_tags: noexport -#+startup: beamer -#+latex_class: beamer -# #+latex_class_options: [bigger] -#+latex_header: \setbeamercovered{transparent} -#+latex: \setbeamertemplate{itemize items}[circle] -#+beamer_color_theme: beaver - -* Are you at the right place? - -We’re in {{{room}}}, for {{{sec}}} ({{{sectime}}}) - -* - -#+latex: \definecolor{darkred}{rgb}{0.8,0,0} -#+latex: {\Large \color{darkred} -#+begin_center -George -#+end_center -#+latex: } - -* - -#+latex: \vspace{-2.5em} -file:./george.png - -#+latex: {\footnotesize -https://www.student.cs.uwaterloo.ca/~se212/george/ask-george/ -#+latex: } - -* Tool support - -Over the years, students have developed a number of tools for using -George and/or editing =.grg= files, such as plugins for Vim and Atom. - -Check them out at - -#+begin_center -Course website → George User Manual → Contributions -#+end_center - -* George mode for Emacs (new!) - -- Syntax highlighting + a number of convenience functions -- Grab it from https://git.sr.ht/~bandali/george-mode \\ - (soon on Contributions page) - -* =a00q01.grg= (demo) - -Walk through answering =a00q01.grg= and submitting on MarkUs - -* Homework 1 -:PROPERTIES: -:BEAMER_act: [<+->] -:END: - -- Let’s do a couple of questions from Homework 1 -- Now you try the rest, let me know if you have any questions diff --git a/se212-f19/se212-t05.org b/se212-f19/se212-t05.org deleted file mode 100644 index a85896d..0000000 --- a/se212-f19/se212-t05.org +++ /dev/null @@ -1,272 +0,0 @@ -#+title: Predicate Logic -#+subtitle: (SE 212 Tutorial 5) -#+author: Amin Bandali -#+email: bandali@uwaterloo.ca -#+date: Wed Oct 9, 2019 -#+language: en -#+options: email:t num:t toc:nil \n:nil ::t |:t ^:t -:t f:t *:t <:t -#+options: tex:t d:nil todo:t pri:nil tags:not-in-toc -#+select_tags: export -#+exclude_tags: noexport -#+startup: beamer -#+latex_class: beamer -# #+latex_class_options: [bigger] -#+latex_header: \setbeamercovered{transparent} -#+latex: \setbeamertemplate{itemize items}[circle] -#+beamer_color_theme: beaver - -* Today’s plan -:PROPERTIES: -:BEAMER_act: [<+->] -:END: - -- do some semantics questions from homework 4 -- do some ND questions from homework 5 - -* =h04q05= - -Provide a counterexample to show that the following argument is not -valid and demonstrate that your answer is correct. - -#+begin_example -forall y : M . exists x : N . p(g(x), y) -|= -exists z : M . p(z, z) -#+end_example - -* =h04q05= \small{(cont’d)} - -#+begin_example -Domain: - M = {m1, m2} - N = {n1, n2} - -Mapping: - Syntax | Meaning - -------------------------- - g(.) | G(n1) := m1 - | G(n2) := m2 - -------------------------- - p(., .) | P(m1, m1) := F - | P(m1, m2) := T - | P(m2, m1) := T - | P(m2, m2) := F -#+end_example - -* =h04q05= \small{(cont’d)} - -#+begin_example -Premise: - [forall y : M . exists x : N . p(g(x), y)] - = [exists x: N. p(g(x), ^m1)] AND - [exists x: N . p(g(x), ^m2)] - = (P(G(n1), m1) OR P(G(n2), m1)) AND - (P(G(n1), m2) OR P(G(n2), m2)) - = (P(m1, m1) OR P(m2, m1)) AND - (P(m1, m2) OR P(m2, m2)) - = (F OR T) AND (T OR F) - = T -#+end_example - -* =h04q05= \small{(cont’d)} - -#+begin_example -Conclusion: - [exists z: M . p(z, z)] - = P(m1, m1) OR P(m2, m2) - = F OR F - = F -#+end_example - -* =h04q06= - -Express the following sentences in predicate logic. Use types in your -formalization. Is the set of formulas consistent? Demonstrate that -your answer is correct using the semantics of predicate logic. - -#+begin_example -All programmer like some computers. -Some programmers use MAC. -Therefore, some people who like some computers use MAC. -#+end_example - -* =h04q06= \small{(cont’d)} - -All programmer like some computers.\\ -Some programmers use MAC.\\ -Therefore, some people who like some computers use MAC. - -#+begin_example -Formalization: - programmer(x) means x is a programmer - usesmac(x) means x uses MAC - likes(x, y) means x likes y - -forall x: Person . programmer(x) => - exists y: Computer . likes(x, y), -exists x: Person . programmer(x) & usesmac(x) -|- -exists x: Person . - (exists y: Computer . likes(x, y) & usesmac(x)) -#+end_example - -* =h04q06= \small{(cont’d)} - -These sentences are /consistent/. Here is an interpretation in which -all the formulas are T: - -#+begin_example -Domain: - People = {John} - Computer = {MacPro} - -Mapping: - Syntax | Meaning - ------------------------------------------- - programmer(.) | programmer(John) = T - likes(.,.) | likes(John, MacPro) = T - usesmac(.) | usesmac(John) = T -#+end_example - -* =h04q06= \small{(cont’d)} - -#+begin_example -formula 1: - [forall x: Person . programmer(x) => - exists y: Computer . likes(x, y)] - = [programmer(^John) => - exists y: Computer . likes(^John, y)]] - = programmer(John) IMP likes(John, MacPro) - = T IMP T - = T - -formula 2: - [exists x: Person . programmer(x) & usesmac(x)] - = programmer(John) AND usesmac(John) - = T AND T - = T -#+end_example - -* =h04q06= \small{(cont’d)} - -#+begin_example -formula 3: - [exists x: Person . (exists y: Computer . - likes(x, y) & usesmac(x))] - = [exists y: Computer . - likes(^John, y) & usesmac(^John)] - = likes(John, MacPro) AND usesmac(John) - = T AND T - = T -#+end_example - -* =h05q01a= - -If the following arguments are valid, use natural deduction AND -semantic tableaux to prove them; otherwise, provide a counterexample. - -#+begin_example -forall x . s(x) | t(x), -forall x . s(x) => t(x) & k(c, x), -forall x . t(x) => m(x) -|- -m(c) -where c is a constant -#+end_example - -* =h05q01a= \small{(cont’d)} - -#+begin_example -#check ND -forall x . s(x) | t(x), -forall x . s(x) => t(x) & k(c, x), -forall x . t(x) => m(x) -|- -m(c) -#+end_example - -* =h05q01a= \small{(cont’d)} - -#+begin_example -1) forall x . s(x) | t(x) premise -2) forall x . s(x) => t(x) & k(c, x) premise -3) forall x . t(x) => m(x) premise -4) s(c) | t(c) by forall_e on 1 -5) s(c) => t(c) & k(c, c) by forall_e on 2 -6) t(c) => m(c) by forall_e on 3 -7) case s(c) { - 8) t(c) & k(c, c) by imp_e on 5, 7 - 9) t(c) by and_e on 8 - 10) m(c) by imp_e on 6, 9 -} -11) case t(c) { - 12) m(c) by imp_e on 6, 11 -} -13) m(c) by cases on 4, 7-10, 11-12 -#+end_example - -* =h05q01b= - -Is this formula a tautology? - -#+begin_example -|- (exists x . p(x)) => forall y . p(y) -#+end_example - -* =h05q01b= \small{(cont’d)} - -No, this formula is not a tautology. Interpretation: - -#+begin_example -1) Domain = {a, b} - -2) Mapping: - Syntax | Meaning - ---------------------- - p(.) | P(a) = T - | P(b) = F - -Conclusion: - [(exists x. p(x)) => forall y. p(y)] -= (P(a) OR P(b)) IMP (P(a) AND P(b)) -= (T OR F) IMP (T AND F) -= T IMP F -= F -#+end_example - -* =h05q01d= - -Is this argument valid? - -#+begin_example -forall x . p(x) | q(x), -forall x . !p(x) -|- -forall x . q(x) -#+end_example - -* =h05q01d= \small{(cont’d)} - -#+begin_example -#check ND - -forall x . p(x) | q(x), forall x . !p(x) |- forall x . q(x) - -1) forall x . p(x) | q(x) premise -2) forall x . !p(x) premise -3) for every xg { - 4) p(xg) | q(xg) by forall_e on 1 - 5) case p(xg) { - 6) !p(xg) by forall_e on 2 - 7) q(xg) by not_e on 5, 6 - } - 8) case q(xg) {} - 9) q(xg) by cases on 4, 5-7, 8-8 -} -10) forall x. q(x) by forall_i on 3-9 -#+end_example - -* Announcements - -- no tutorial next week (Oct 16) (reading week) -- no tutorial the week after (Oct 23) (midterm marking) diff --git a/static/se212-f19/se212-h02q04d-soln.grg b/static/se212-f19/se212-h02q04d-soln.grg new file mode 100644 index 0000000..e395717 --- /dev/null +++ b/static/se212-f19/se212-h02q04d-soln.grg @@ -0,0 +1,25 @@ +#u abandali +#a h02 + +#q q04d + +p <=> q, p & q <=> (p | q) + +#check TP + +p <=> q <-> p & q <=> (p | q) + + 1) p & q <=> (p | q) + 2) (p & q => p | q) & (p | q => p & q) by equiv + 3) (!(p & q) | p | q) & (!(p | q) | p & q) by impl * 2 + 4) (!p | !q | p | q) & (!(p | q) | p & q) by dm + 5) (true | !q | q) & (!(p | q) | p & q) by lem + 6) true & (!(p | q) | p & q) by simp1 + 7) !(p | q) | p & q by simp1 + 8) !p & !q | p & q by dm + 9) (!p & !q | p) & (!p & !q | q) by distr +10) (!p | p) & (!q | p) & (!p | q) & (!q | q) by distr * 2 +11) true & (!q | p) & (!p | q) & true by lem * 2 +12) (!q | p) & (!p | q) by simp1 * 2 +13) (q => p) & (p => q) by impl * 2 +14) p <=> q by equiv diff --git a/static/se212-f19/se212-t01.html b/static/se212-f19/se212-t01.html new file mode 100644 index 0000000..d81cbd7 --- /dev/null +++ b/static/se212-f19/se212-t01.html @@ -0,0 +1,343 @@ + + + + + + + +Propositional Logic + + + + + + +
+

Propositional Logic +
+(SE 212 TUT 102) +

+ +
+

1 Are you at the right place?

+
+

+We’re in MC 4040, for SE 212 TUT 102 (03:30-04:20W) +

+
+
+ +
+

2

+
+
+

+George +

+
+
+
+ + + +
+

4 Tool support

+
+

+Over the years, students have developed a number of tools for using +George and/or editing .grg files, such as plugins for Vim and Atom. +

+ +

+Check them out at +

+ +
+

+Course website → George User Manual → Contributions +

+
+
+
+ +
+

5 George mode for Emacs (new!)

+
+ +
+
+ +
+

6 a00q01.grg (demo)

+
+

+Walk through answering a00q01.grg and submitting on MarkUs +

+
+
+ +
+

7 Homework 1

+
+
    +
  • Let’s do a couple of questions from Homework 1
    • +
  • Now you try the rest, let me know if you have any questions
    • +
+
+
+
+
+

Date: Wed Sep 11, 2019

+

Author: Amin Bandali

+ +

Created: 2019-09-18 Wed 23:12

+

Validate

+
+ + diff --git a/static/se212-f19/se212-t01.org b/static/se212-f19/se212-t01.org new file mode 100644 index 0000000..12e9cdd --- /dev/null +++ b/static/se212-f19/se212-t01.org @@ -0,0 +1,78 @@ +#+macro: topic Propositional Logic + +#+macro: room MC 4040 +#+macro: sec1 SE 212 TUT 101 +#+macro: sec2 SE 212 TUT 102 +#+macro: time1 02:30-03:20W +#+macro: time2 03:30-04:20W + +#+macro: sec {{{sec2}}} +#+macro: sectime {{{time2}}} + +#+title: {{{topic}}} +#+subtitle: ({{{sec}}}) +#+author: Amin Bandali +#+email: bandali@uwaterloo.ca +#+date: Wed Sep 11, 2019 +#+language: en +#+options: email:t num:t toc:nil \n:nil ::t |:t ^:t -:t f:t *:t <:t +#+options: tex:t d:nil todo:t pri:nil tags:not-in-toc +#+select_tags: export +#+exclude_tags: noexport +#+startup: beamer +#+latex_class: beamer +# #+latex_class_options: [bigger] +#+latex_header: \setbeamercovered{transparent} +#+latex: \setbeamertemplate{itemize items}[circle] +#+beamer_color_theme: beaver + +* Are you at the right place? + +We’re in {{{room}}}, for {{{sec}}} ({{{sectime}}}) + +* + +#+latex: \definecolor{darkred}{rgb}{0.8,0,0} +#+latex: {\Large \color{darkred} +#+begin_center +George +#+end_center +#+latex: } + +* + +#+latex: \vspace{-2.5em} +file:./george.png + +#+latex: {\footnotesize +https://www.student.cs.uwaterloo.ca/~se212/george/ask-george/ +#+latex: } + +* Tool support + +Over the years, students have developed a number of tools for using +George and/or editing =.grg= files, such as plugins for Vim and Atom. + +Check them out at + +#+begin_center +Course website → George User Manual → Contributions +#+end_center + +* George mode for Emacs (new!) + +- Syntax highlighting + a number of convenience functions +- Grab it from https://git.sr.ht/~bandali/george-mode \\ + (soon on Contributions page) + +* =a00q01.grg= (demo) + +Walk through answering =a00q01.grg= and submitting on MarkUs + +* Homework 1 +:PROPERTIES: +:BEAMER_act: [<+->] +:END: + +- Let’s do a couple of questions from Homework 1 +- Now you try the rest, let me know if you have any questions diff --git a/static/se212-f19/se212-t05.org b/static/se212-f19/se212-t05.org new file mode 100644 index 0000000..a85896d --- /dev/null +++ b/static/se212-f19/se212-t05.org @@ -0,0 +1,272 @@ +#+title: Predicate Logic +#+subtitle: (SE 212 Tutorial 5) +#+author: Amin Bandali +#+email: bandali@uwaterloo.ca +#+date: Wed Oct 9, 2019 +#+language: en +#+options: email:t num:t toc:nil \n:nil ::t |:t ^:t -:t f:t *:t <:t +#+options: tex:t d:nil todo:t pri:nil tags:not-in-toc +#+select_tags: export +#+exclude_tags: noexport +#+startup: beamer +#+latex_class: beamer +# #+latex_class_options: [bigger] +#+latex_header: \setbeamercovered{transparent} +#+latex: \setbeamertemplate{itemize items}[circle] +#+beamer_color_theme: beaver + +* Today’s plan +:PROPERTIES: +:BEAMER_act: [<+->] +:END: + +- do some semantics questions from homework 4 +- do some ND questions from homework 5 + +* =h04q05= + +Provide a counterexample to show that the following argument is not +valid and demonstrate that your answer is correct. + +#+begin_example +forall y : M . exists x : N . p(g(x), y) +|= +exists z : M . p(z, z) +#+end_example + +* =h04q05= \small{(cont’d)} + +#+begin_example +Domain: + M = {m1, m2} + N = {n1, n2} + +Mapping: + Syntax | Meaning + -------------------------- + g(.) | G(n1) := m1 + | G(n2) := m2 + -------------------------- + p(., .) | P(m1, m1) := F + | P(m1, m2) := T + | P(m2, m1) := T + | P(m2, m2) := F +#+end_example + +* =h04q05= \small{(cont’d)} + +#+begin_example +Premise: + [forall y : M . exists x : N . p(g(x), y)] + = [exists x: N. p(g(x), ^m1)] AND + [exists x: N . p(g(x), ^m2)] + = (P(G(n1), m1) OR P(G(n2), m1)) AND + (P(G(n1), m2) OR P(G(n2), m2)) + = (P(m1, m1) OR P(m2, m1)) AND + (P(m1, m2) OR P(m2, m2)) + = (F OR T) AND (T OR F) + = T +#+end_example + +* =h04q05= \small{(cont’d)} + +#+begin_example +Conclusion: + [exists z: M . p(z, z)] + = P(m1, m1) OR P(m2, m2) + = F OR F + = F +#+end_example + +* =h04q06= + +Express the following sentences in predicate logic. Use types in your +formalization. Is the set of formulas consistent? Demonstrate that +your answer is correct using the semantics of predicate logic. + +#+begin_example +All programmer like some computers. +Some programmers use MAC. +Therefore, some people who like some computers use MAC. +#+end_example + +* =h04q06= \small{(cont’d)} + +All programmer like some computers.\\ +Some programmers use MAC.\\ +Therefore, some people who like some computers use MAC. + +#+begin_example +Formalization: + programmer(x) means x is a programmer + usesmac(x) means x uses MAC + likes(x, y) means x likes y + +forall x: Person . programmer(x) => + exists y: Computer . likes(x, y), +exists x: Person . programmer(x) & usesmac(x) +|- +exists x: Person . + (exists y: Computer . likes(x, y) & usesmac(x)) +#+end_example + +* =h04q06= \small{(cont’d)} + +These sentences are /consistent/. Here is an interpretation in which +all the formulas are T: + +#+begin_example +Domain: + People = {John} + Computer = {MacPro} + +Mapping: + Syntax | Meaning + ------------------------------------------- + programmer(.) | programmer(John) = T + likes(.,.) | likes(John, MacPro) = T + usesmac(.) | usesmac(John) = T +#+end_example + +* =h04q06= \small{(cont’d)} + +#+begin_example +formula 1: + [forall x: Person . programmer(x) => + exists y: Computer . likes(x, y)] + = [programmer(^John) => + exists y: Computer . likes(^John, y)]] + = programmer(John) IMP likes(John, MacPro) + = T IMP T + = T + +formula 2: + [exists x: Person . programmer(x) & usesmac(x)] + = programmer(John) AND usesmac(John) + = T AND T + = T +#+end_example + +* =h04q06= \small{(cont’d)} + +#+begin_example +formula 3: + [exists x: Person . (exists y: Computer . + likes(x, y) & usesmac(x))] + = [exists y: Computer . + likes(^John, y) & usesmac(^John)] + = likes(John, MacPro) AND usesmac(John) + = T AND T + = T +#+end_example + +* =h05q01a= + +If the following arguments are valid, use natural deduction AND +semantic tableaux to prove them; otherwise, provide a counterexample. + +#+begin_example +forall x . s(x) | t(x), +forall x . s(x) => t(x) & k(c, x), +forall x . t(x) => m(x) +|- +m(c) +where c is a constant +#+end_example + +* =h05q01a= \small{(cont’d)} + +#+begin_example +#check ND +forall x . s(x) | t(x), +forall x . s(x) => t(x) & k(c, x), +forall x . t(x) => m(x) +|- +m(c) +#+end_example + +* =h05q01a= \small{(cont’d)} + +#+begin_example +1) forall x . s(x) | t(x) premise +2) forall x . s(x) => t(x) & k(c, x) premise +3) forall x . t(x) => m(x) premise +4) s(c) | t(c) by forall_e on 1 +5) s(c) => t(c) & k(c, c) by forall_e on 2 +6) t(c) => m(c) by forall_e on 3 +7) case s(c) { + 8) t(c) & k(c, c) by imp_e on 5, 7 + 9) t(c) by and_e on 8 + 10) m(c) by imp_e on 6, 9 +} +11) case t(c) { + 12) m(c) by imp_e on 6, 11 +} +13) m(c) by cases on 4, 7-10, 11-12 +#+end_example + +* =h05q01b= + +Is this formula a tautology? + +#+begin_example +|- (exists x . p(x)) => forall y . p(y) +#+end_example + +* =h05q01b= \small{(cont’d)} + +No, this formula is not a tautology. Interpretation: + +#+begin_example +1) Domain = {a, b} + +2) Mapping: + Syntax | Meaning + ---------------------- + p(.) | P(a) = T + | P(b) = F + +Conclusion: + [(exists x. p(x)) => forall y. p(y)] += (P(a) OR P(b)) IMP (P(a) AND P(b)) += (T OR F) IMP (T AND F) += T IMP F += F +#+end_example + +* =h05q01d= + +Is this argument valid? + +#+begin_example +forall x . p(x) | q(x), +forall x . !p(x) +|- +forall x . q(x) +#+end_example + +* =h05q01d= \small{(cont’d)} + +#+begin_example +#check ND + +forall x . p(x) | q(x), forall x . !p(x) |- forall x . q(x) + +1) forall x . p(x) | q(x) premise +2) forall x . !p(x) premise +3) for every xg { + 4) p(xg) | q(xg) by forall_e on 1 + 5) case p(xg) { + 6) !p(xg) by forall_e on 2 + 7) q(xg) by not_e on 5, 6 + } + 8) case q(xg) {} + 9) q(xg) by cases on 4, 5-7, 8-8 +} +10) forall x. q(x) by forall_i on 3-9 +#+end_example + +* Announcements + +- no tutorial next week (Oct 16) (reading week) +- no tutorial the week after (Oct 23) (midterm marking)