{"id":19838,"date":"2026-09-14T08:13:52","date_gmt":"2026-09-14T08:13:52","guid":{"rendered":"http:\/\/www.max-sperling.bplaced.net\/?p=19838"},"modified":"2026-09-14T08:25:34","modified_gmt":"2026-09-14T08:25:34","slug":"math-exercise-12-logic","status":"publish","type":"post","link":"http:\/\/www.max-sperling.bplaced.net\/?p=19838","title":{"rendered":"Math \u2013 Exercise 12 (Logic)"},"content":{"rendered":"<p>Topics: Deductive reasoning (linear temporal logic aka LTL)<\/p>\n<hr>\n<p><strong>Given<\/strong><\/p>\n<p>If the server detects an error, it will eventually enter recovery mode. [1]<br \/>\nThe server remains in recovery mode until the error is resolved. [2]<br \/>\nIf the error is resolved, the server will eventually return to normal operation. [3]<br \/>\nThe server has detected an error now. [4]<\/p>\n<hr>\n<p><strong>Find<\/strong><\/p>\n<p>Will the server eventually return to normal operation?<\/p>\n<hr>\n<p><strong>Solution<\/strong><\/p>\n<p>Definition:<br \/>\nE: The server has detected an error.<br \/>\nR: The server is in recovery mode.<br \/>\nN: The server is operating normally.<br \/>\n(X: Next \u2014 X\u03c6 means that \u03c6 is true at the next moment.)<br \/>\nF: Eventually \u2014 F\u03c6 means that \u03c6 will be true at some future point.<br \/>\nG: Always \u2014 G\u03c6 means that \u03c6 is true at all future points.<br \/>\nU: Until \u2014 \u03c6U\u03c8 means that \u03c6 remains true until \u03c8 becomes true.<\/p>\n<p>Representation:<br \/>\n[1]: G(E\u2192FR)<br \/>\n[2]: G(R\u2192(RU\u00acE))<br \/>\n[3]: G(\u00acE\u2192FN)<br \/>\n[4]: E<\/p>\n<p>Deduction:<br \/>\nE &#8212;[1]&#8212;> \u200bFR &#8212;[2]&#8212;> \u200bRU\u00acE &#8212;[3]&#8212;> \u200bFN<\/p>\n<hr>\n<p><strong>Answer<\/strong><\/p>\n<p>Yes, the server will eventually return to normal operation.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Topics: Deductive reasoning (linear temporal logic aka LTL) Given If the server detects an error, it will eventually enter recovery<\/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\/19838"}],"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=19838"}],"version-history":[{"count":24,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=\/wp\/v2\/posts\/19838\/revisions"}],"predecessor-version":[{"id":19862,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=\/wp\/v2\/posts\/19838\/revisions\/19862"}],"wp:attachment":[{"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=19838"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=19838"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.max-sperling.bplaced.net\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=19838"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}