{"id":19863,"date":"2026-09-14T09:02:59","date_gmt":"2026-09-14T09:02:59","guid":{"rendered":"http:\/\/www.max-sperling.bplaced.net\/?p=19863"},"modified":"2026-09-14T09:23:22","modified_gmt":"2026-09-14T09:23:22","slug":"math-exercise-13-logic","status":"publish","type":"post","link":"http:\/\/www.max-sperling.bplaced.net\/?p=19863","title":{"rendered":"Math \u2013 Exercise 13 (Logic)"},"content":{"rendered":"<p>Topics: Deductive reasoning (first-order computation tree logic aka FO-CTL)<\/p>\n<hr>\n<p><strong>Given<\/strong><\/p>\n<ul>\n<li>Every user who submits a request will eventually receive a receipt on every possible notification path. [1]<\/li>\n<li>If a user receives a receipt, then on every possible notification path the user will eventually receive a confirmation. [2]<\/li>\n<li>Alice has submitted a request. [3]<\/li>\n<li>Alice is a user. [4]<\/li>\n<\/ul>\n<hr>\n<p><strong>Find<\/strong><\/p>\n<p>Will Alice eventually receive a confirmation on every possible notification path?<\/p>\n<hr>\n<p><strong>Solution<\/strong><\/p>\n<p>Definition:<br \/>\nU(x): x is a user.<br \/>\nR<sub>1<\/sub>(x): x has submitted a request.<br \/>\nR<sub>2<\/sub>(x): x has received a receipt.<br \/>\nC(x): x has received a confirmation.<br \/>\nA: All paths \u2014 A\u03c6 means that \u03c6 is true on all possible future paths.<br \/>\n(- E: Exists a path \u2014 E\u03c6 means that \u03c6 is true on at least one possible future path.)<br \/>\nAdditional: LTL operators (X, F, G, U), see <a href=\"http:\/\/www.max-sperling.bplaced.net\/?p=19838\">Math \u2013 Exercise 12 (Logic)<\/a>.<\/p>\n<p>Representation:<br \/>\n[1]: \u2200x AG((U(x)\u2227R<sub>1<\/sub>(x))\u2192AF R<sub>2<\/sub>(x))<br \/>\n[2]: \u2200x AG(R<sub>2<\/sub>(x)\u2192AF C(x))<br \/>\n[3]: R<sub>1<\/sub>(Alice)<br \/>\n[4]: U(Alice)<\/p>\n<p>Deduction:<br \/>\nInstantiate x=Alice in [1]: \u2200x AG((U(Alice)\u2227R<sub>1<\/sub>(Alice))\u2192AF R<sub>2<\/sub>(Alice)),<br \/>\nwith [3] and [4] we conclude: AF R<sub>2<\/sub>(Alice).<br \/>\nInstantiate x=Alice in [2]: \u2200x AG(R<sub>2<\/sub>(Alice)\u2192AF C(Alice)),<br \/>\nwith AF R<sub>2<\/sub>(Alice) we conclude: AF C(Alice).<\/p>\n<hr>\n<p><strong>Answer<\/strong><\/p>\n<p>Yes, Alice will eventually receive a confirmation on every possible notification path.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Topics: Deductive reasoning (first-order computation tree logic aka FO-CTL) Given Every user who submits a request will eventually receive a<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"inline_featured_image":false},"categories":[47],"tags":[],"_links":{"self":[{"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=\/wp\/v2\/posts\/19863"}],"collection":[{"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=19863"}],"version-history":[{"count":15,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=\/wp\/v2\/posts\/19863\/revisions"}],"predecessor-version":[{"id":19878,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=\/wp\/v2\/posts\/19863\/revisions\/19878"}],"wp:attachment":[{"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=19863"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=19863"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=19863"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}