199.107 Non-monotonic Extension of Temporal Logic
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2023S, VU, 2.0h, 3.0EC


  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Präsenz


Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

  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

Inhalt der Lehrveranstaltung

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.



further information will be announced



Weitere Informationen

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

Vortragende Personen


LVA Termine

Mi.10:00 - 12:0031.05.2023Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
Do.10:00 - 12:0001.06.2023 - 22.06.2023Seminarraum FAV EG C (Seminarraum Gödel) Lecture
Di.10:00 - 12:0006.06.2023 - 27.06.2023FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) Lecture
Mi.10:00 - 12:0007.06.2023Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
Di.10:00 - 12:0013.06.2023EI 5 Hochenegg HS Lecture
Do.10:00 - 12:0029.06.2023Seminarraum FAV EG C (Seminarraum Gödel) Exam
Non-monotonic Extension of Temporal Logic - Einzeltermine
Mi.31.05.202310:00 - 12:00Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
Do.01.06.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture
Di.06.06.202310:00 - 12:00FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) Lecture
Mi.07.06.202310:00 - 12:00Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
Di.13.06.202310:00 - 12:00EI 5 Hochenegg HS Lecture
Do.15.06.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture
Di.20.06.202310:00 - 12:00FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) Lecture
Do.22.06.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Lecture
Di.27.06.202310:00 - 12:00FAV Hörsaal 3 Zemanek (Seminarraum Zemanek) Lecture
Do.29.06.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Exam


further information will be announced


Von Bis Abmeldung bis
30.01.2023 00:00 29.05.2023 23:59


Please register in TISS.


PhD TU Wien Informatics Doctoral School Keine Angabe


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


Required background knowledge: fundamentals of classical logic.

Weitere Informationen

  • Anwesenheitspflicht!