Non-Monotonic Extension
of Temporal Logic
Pedro Cabalar. TU Wien, PhD Course

Slides

• Unit 0. ASP in 15 minutes

• Unit 1. Equilibrium Logic

  • htcheck-distrib.zip: a simple toolkit for HT logic

  • Exercises bulletin (3'5 points) + 0,5 extra with blackboard presentation

    1. Prove that any (reduct-based) stable model is a classical model

    2. Prove persistence in HT and that negation is only evaluated in T

    3. Prove that p v ¬p and ¬¬p -> p are not HT-valid but are HT-equivalent

    4. Prove that ¬p -> q strongly entails p v q

    5. Compute the truth tables for G3: justify the one for implication 

    6. Compute the number of different programs for 2 and 3 variables

• Unit 2. (Monotonic) Temporal Logics for Linear Traces

  • online exercises: formalising some natural language sentences with LTL

  • Büchi automata generator for LTL formulas

  • Second bulletin (3 points) + 0,5 extra with blackboard presentation

• Unit 3: Non-Monotonic Extension of Temporal Logics

  • Third bulletin (3 points) + 0,5 extra with blackboard presentation

• Points collected (June 28th, 2023) with submissions and blackboard exercises

Bibliography

• [Aguado et al. (2020)] Felicidad Aguado, Pedro Cabalar, Martín Diéguez, Gilberto Pérez, Torsten Schaub, Anna Schuhmann and Concepción Vidal. Linear-Time Temporal Answer Set Programming. Theory and Practice of Logic Programming 23(1), pp. 2–56, 2020.

• [van Dalen (2008)] Dirk van Dalen. Logic and Structure, Springer, 2008.

• [Demri et al (2016)] Stéphane Demri, Valentin Goranko and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems, Cambridge T.C.S. 2016.

• [Lifschitz (2019)] Vladimir Lifschitz. Answer Set Programming, Springer, 2019.