X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/4927af92d3b136436aa41a26369794443aa69b97..c468ea86fe03b0000d6377079118da7e78e6ca4f:/se212-f19/se212-t05.org 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/se212-f19/se212-t05.org b/se212-f19/se212-t05.org new file mode 120000 index 0000000..3588c67 --- /dev/null +++ b/se212-f19/se212-t05.org @@ -0,0 +1 @@ +../../site-files/se212-f19/se212-t05.org \ No newline at end of file