{"id":7091,"date":"2024-03-08T23:13:14","date_gmt":"2024-03-08T15:13:14","guid":{"rendered":"http:\/\/tsinghualogic.net\/JRC\/?page_id=7091"},"modified":"2024-03-08T23:13:16","modified_gmt":"2024-03-08T15:13:16","slug":"short-term-course","status":"publish","type":"page","link":"http:\/\/tsinghualogic.net\/JRC\/short-term-course\/","title":{"rendered":"Short-term course"},"content":{"rendered":"\n

Temporal Logics and Tableaux<\/h2>\n\n\n\n

Lecturer<\/strong>: Valentin Goranko<\/p>\n\n\n\n

Location<\/strong>: Room 3513, Teaching Building No.3, Tsinghua University<\/p>\n\n\n\n

Time<\/strong>: Wednesday 9:50-12:15, from March 20th to May 8th, 2024.<\/p>\n\n\n\n

==Course Description==<\/h3>\n\n\n\n

This course will introduce and discuss some of the most important types and systems of temporal logics, including instant-based logics of linear and branching time, as well as some temporal logics for multi- agent systems. The course will also present tableaux-based decision methods for some of these logics. Time permitting, it may also cover a selection of additional topics, such as interval-based temporal logics, temporal-epistemic logics, or first-order temporal logics.<\/p>\n\n\n\n

The course is intended as interdisciplinary, for a broad audience of mainly graduate students interested in logical, philosophical, and computational aspects of temporal reasoning.<\/p>\n\n\n\n

==Outline of Main Topics and Tentative Schedule==<\/h3>\n\n\n\n

The course will comprise six 135-minute long lecture sessions, tentatively planned as follows:<\/p>\n\n\n\n

Lecture session 1.<\/strong><\/p>\n\n\n\n

    \n
  • Introduction. Reasoning about time: brief history and philosophical origins. Time, tense, and modality. Models and properties of time flows.<\/li>\n\n\n\n
  • Prior\u2019s basic temporal logic and some extensions of it.
    Temporal logics over linear time flows. Additional temporal operators: Nexttime, Since, and Until. The linear time temporal logic LTL (briefly).<\/li>\n<\/ul>\n\n\n\n

    Lecture session 2.<\/strong><\/p>\n\n\n\n

      \n
    • Diodorus\u2019 Master Argument and related arguments formalised.
      Branching time temporal logics as possible solutions. Models of branching time and historical necessity.<\/li>\n\n\n\n
    • Peircean branching time temporal logics. Ockhamist branching time temporal logics. Branching time temporal logics in computer science: CTL and CTL* (briefly).<\/li>\n<\/ul>\n\n\n\n

      Lecture session 3.<\/strong><\/p>\n\n\n\n

        \n
      • Tableaux-based methods for modal and temporal logics:<\/li>\n<\/ul>\n\n\n\n

        \u2013 preliminaries on tableaux for classical propositional logic.<\/p>\n\n\n\n

        \u2013 a general framework for the incremental tableaux method: main components and closures of formulae, full expansions, pre-tableaux construction phase and initial tableaux, elimination phase and final tableaux. Open and closed tableaux and constructing models from open tableaux.<\/p>\n\n\n\n

        Lecture session 4.<\/strong><\/p>\n\n\n\n

          \n
        • Incremental tableaux-based decision procedures for the temporal logics LTL and CTL.<\/li>\n<\/ul>\n\n\n\n

          Lecture session 5.<\/strong><\/p>\n\n\n\n

            \n
          • Alternating time temporal logic ATL and some variations and extensions. Outline of tableaux for ATL.<\/li>\n<\/ul>\n\n\n\n

            Lecture session 6.<\/strong><\/p>\n\n\n\n

              \n
            • The temporal logic of coalitional goal assignments TLCGA and some variations.<\/li>\n<\/ul>\n\n\n\n

              Alternative optional topics.<\/strong><\/p>\n\n\n\n

              1. Interval-based temporal logics on linear time flows. 2. Temporal epistemic logics.
              3. First-order temporal logics.<\/p>\n\n\n\n

              ==Expected Level and Pre-requisites==<\/h3>\n\n\n\n

              The course is intended for a broad audience with basic knowledge of classical and modal logics. The intended level is middle graduate, but it can be adjusted up or down, depending on the actual audience.<\/p>\n\n\n\n

              ==Selected references==<\/h3>\n\n\n\n
                \n
              1. Valentin Goranko. Temporal Logics, Cambridge University Press, 2023.<\/li>\n\n\n\n
              2. Valentin Goranko and Antje Rumberg. Temporal Logic, Stanford Encyclopedia of Philosophy, 2024.<\/li>\n\n\n\n
              3. John Burgess. Basic tense logic, in Gabbay and Guenthner (eds.), Handbook of Philosophical Logic, 2nd edition, Volume 7, Gabbay and Guenthner (eds.) (2002), pp. 142.<\/li>\n\n\n\n
              4. St \u0301ephane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science. CUP, 2016.<\/li>\n\n\n\n
              5. Rob Goldblatt. Logics of Time and Computations. CSLI pubblications, 2nd revised and expanded edition, 1992.<\/li>\n\n\n\n
              6. P. \u00d8hrstr\u00f8m and Per Hasle. Temporal Logic: From Ancient Ideas to Artificial Intelligence. Kluwer, 1995. (Reprinted by Springer).<\/li>\n\n\n\n
              7. A.N. Prior. Past, Present and Future. Oxford University Press, 1967.<\/li>\n\n\n\n
              8. Yde Venema. Temporal Logic, chapter in: Lou Goble (ed), Blackwell Guide on Philosophical Logic,Blackwell Publishers, 2001, pp 203-211<\/li>\n<\/ol>\n\n\n\n

                Relevant parts of these plus additional readings will be made available to the participants in the course.<\/p>\n","protected":false},"excerpt":{"rendered":"

                Temporal Logics and Tableaux Lecturer: Valentin Goranko […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7091"}],"collection":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/comments?post=7091"}],"version-history":[{"count":1,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7091\/revisions"}],"predecessor-version":[{"id":7092,"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/pages\/7091\/revisions\/7092"}],"wp:attachment":[{"href":"http:\/\/tsinghualogic.net\/JRC\/wp-json\/wp\/v2\/media?parent=7091"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}