htcheck-distrib.zip: a simple toolkit for HT logic
Exercises bulletin (3'5 points) + 0,5 extra with blackboard presentation
Prove that any (reduct-based) stable model is a classical model
Prove persistence in HT and that negation is only evaluated in T
Prove that p v ¬p and ¬¬p -> p are not HT-valid but are HT-equivalent
Prove that ¬p -> q strongly entails p v q
Compute the truth tables for G3: justify the one for implication
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
[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.