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

Description:
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 G₃ (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 G₃. 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

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

further information will be announced

Please register in TISS.

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