199.107 Non-monotonic Extension of Temporal Logic
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2023S, VU, 2.0h, 3.0EC


  • Semester hours: 2.0
  • Credits: 3.0
  • Type: VU Lecture and Exercise
  • Format: Presence

Learning outcomes

After successful completion of the course, students are able to...

  1. Learning the basis of the non-monotonic formalism of Equilibrium Logic
  2. Acquiring knowledge about monotonic temporal logics based on linear traces
  3. Being able to identify natural language sentences as temporal formulas and vice versa
  4. Understanding the properties of non-monotonic extensions of temporal logic


Subject of course

Non-monotonic reasoning allows extracting conclusions from absence of information, possibly retracting them if new information is available. The course will cover extensions of several Temporal Logics based on linear time (such as LTL, LDL, or Metric Temporal Logic) to incorporate non-monotonic reasoning, choosing some temporal traces that are said to be in equilibrium. In the non-temporal case, these equilibrium models are obtained by a selection among models from Gödel’s three-valued logic. We start describing their properties and their relation to logic programs, where they correspond to so-called answer sets. We will then introduce several (monotonic) Temporal Logics, their syntax, semantics and relation to different types of automata. Finally, we will extend these logics, defining temporal equilibrium models, presenting the associated results and their use in implemented systems for temporal logic programming.

Three Units:

U1. Equilibrium Logic.

Gödel’s logic G3 (or Logic of Here-and-There, HT). Semantics and Inference. Equilibrium Models. Relation to Answer Set Programming (ASP). Strong Equivalence and Strong En- tailment. Explicit Negation. Quantified Equilibrium Logic. Reduction to Classical Logic (star-transformation).

U2. (Monotonic) Temporal Logics for Linear Traces.

LTL Syntax and semantics. Formalisation of properties. Expressiveness and Complexity. Relation to automata; model checking. Kamp’s Translation to First Order Logic. Infinite vs. Finite traces. Other temporal logics based on linear traces: LDL, MTL.

U3. Non-Monotonic Extension of Temporal Logics.

Temporal HT, Temporal G3. Temporal Equilibrium Logic (TEL). Relation to ASP. Strong Equivalence. From TEL to (quantified) LTL. From TEL to automata. Equilibrium LDL and MTL. Temporal Logic Programs: tools telingo, abstem. Knowledge Representation for temporal domains.

Course schedule:

The course will be held from E/May - E/June. Further information will be announced.

Teaching methods

further information will be announced

Mode of examination


Additional information

The lecturer of this course will be Pedro Cabalar / University of A Coruña, SPAIN.

This is a guest professor course of the TU Wien Informatics Doctoral School. It is targeted to Doctoral Students of the Faculty of Informatics, but, subject to availability of free seats, open to all PhD students and interested Master students.


Workload - ECTS breakdown - total 75 hours:
Lectures - in the class: 16h
Discussion of exercises - in the class: 3.5h
Oral exam (if applicable) - in the class: 0.5h
Solving exercises - at home: 30h
Further reading - at home: 24h



Course dates

Wed10:00 - 12:0031.05.2023Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
Thu10:00 - 12:0001.06.2023 - 22.06.2023Seminarraum FAV EG C (Seminarraum Gödel) Lecture
Tue10:00 - 12:0006.06.2023 - 27.06.2023FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) Lecture
Wed10:00 - 12:0007.06.2023Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
Tue10:00 - 12:0013.06.2023EI 5 Hochenegg HS Lecture
Thu10:00 - 12:0029.06.2023Seminarraum FAV EG C (Seminarraum Gödel) Exam
Non-monotonic Extension of Temporal Logic - Single appointments
Wed31.05.202310:00 - 12:00Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
Thu01.06.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture
Tue06.06.202310:00 - 12:00FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) Lecture
Wed07.06.202310:00 - 12:00Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
Tue13.06.202310:00 - 12:00EI 5 Hochenegg HS Lecture
Thu15.06.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture
Tue20.06.202310:00 - 12:00FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) Lecture
Thu22.06.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture
Tue27.06.202310:00 - 12:00FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) Lecture
Thu29.06.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Exam

Examination modalities

further information will be announced

Course registration

Begin End Deregistration end
30.01.2023 00:00 29.05.2023 23:59

Registration modalities

Please register in TISS.


Study CodeObligationSemesterPrecon.Info
PhD TU Wien Informatics Doctoral School Not specified


[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 Pro- gramming. 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.

Previous knowledge

Required background knowledge: fundamentals of classical logic.


  • Attendance Required!