
| Session 1: Invited talk | ||
| 09:30 - 10:30 | Franz Baader | Automata and Tableaux methods for Description and Modal Logics |
| 10:30 - 11:00 | Coffee break | |
| Session 2: Type Theories and Logical Frameworks | ||
| 11:00 - 11:30 | Serge Autexier, Carsten Schuermann | Disproving False Conjectures |
| 11:30 - 12:00 | F.J. Martín-Mateos, J.A. Alonso, M.J. Hidalgo, J.L. Ruiz-Reina. | A Formal Proof of Dickson's Lemma in ACL2 |
| 12:00 - 12:30 | Alberto Ciaffaglione, Luigi Liquori, Marino Miculan | Imperative Object-based Calculi in (Co)Inductive Type Theories |
| 12:30 - 14:00 | Lunch | |
| Session 3: invited talk | ||
| 14:00 - 15:00 | Sergei Goncharov | TBA |
| Session 4: Verification | ||
| 15:00 - 15:30 | Robert Nieuwenhuis, Albert Oliveras | Congruence Closure with Integer Offsets |
| 15:30 - 16:00 | Christoph Walther, Stephan Schweitzer | A Machine-Verified Code Generator |
| 16:00 - 16:30 | Coffee break | |
| Session 5: Non-Classical Logics | ||
| 16:30 - 17:00 | Matthias Baaz, Christian Fermueller | A Translation Characterizing the Constructive Content of Classical Theories |
| 17:00 - 17:30 | Sebastian Brandt, Anni-Yasmin Turhan, Ralf Küsters | Extensions of Non-standard Inferences to Description Logics with Transitive Roles |
| 17:30 - 18:00 | Bernhard Heinemann | Extended Canonicity of Certain Topological Properties of Set Spaces |
| 18:00 - 18:30 | Silvio Ghilardi, Luigi Santocanale | Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics |
| 19:00 Welcoming dinner | ||
| Session 6: Invited talk | ||
| 09:30 - 10:30 | Dexter Kozen | TBA |
| Coffee break | ||
| Session 7: Rewriting | ||
| 11:00 - 11:30 | Juergen Giesl, Rene Thiemann, Peter Schneider-Kamp, Stephan Falke | Improving Dependency Pairs |
| 11:30 - 12:00 | Kumar Neeraj Verma | On Closure under Complementation of Equational Tree Automata for Theories |
| 12:00 - 12:30 | Barbara Morawska | Completeness of E-unification with eager Variable Elimination |
| 12:30 - 14:00 | Lunch | |
| Session 8: invited talk | ||
| 14:00 - 15:00 | Serikjan Badaev | Computable Numberings |
| Session 9: Temporal Logics and Games | ||
| 15:00 - 15:30 | Boris Konev, Anatoli Degtyarev, Michael Fisher | Handling Equality in Monodic Temporal Resolution |
| 15:30 - 16:00 | Dietmar Berwanger, Erich Graedel, Stephan Kreutzer | Once upon a Time in the West -- Determinacy, Definability and Complexity of Path Games |
| 16:00 - 16:30 | Coffee break | |
| Session 10: Non-Monotonic Reasoning | ||
| 16:30 - 17:00 | Davy Van Nieuwenborgh, Dirk Vermeir | Ordered Diagnosis |
| 17:00 - 17:30 | Toshiko Wakaki, Katsumi Inoue, Chiaki Sakama, Katsumi Nitta | Computing Preferred Answer Sets in Answer Sets Programming |
| 17:30 - 18:00 | Quoc Bao Vo, Abhaya Nayak, Norman Foo | A Syntax-Based Approach to Reasoning About Action |
| 10:00-18:00 Excursion | ||
| 19:00 Conference dinner |
| Session 11: Invited talk | ||
| 09:30 - 10:30 | Thomas Wilke | Minimizing automata on infinite words |
| Coffee break | ||
| Session 12 | ||
| 11:00 - 11:30 | Margarita Korovina | Fixed Points on Continuous Data Types |
| 11:30 - 12:00 | Martin Fränzle, Christian Herde | Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems |
| 12:00 - 12:30 | Thierry Boy de la Tour, Mnacho Echenim | NP-Completeness Results for Deductive Problems on Stratified Terms |
| 12:30 - 14:00 | Lunch | |
| Session 13: Automata and Words | ||
| 14:00 - 14:30 | Dietrich Kuske | Is Cantor's Theorem Automatic? |
| 14:30 - 15:00 | Markus Lohrey | Automatic Structures of Bounded Degree |
| Session 14: Reasoning with Probabilities | ||
| 15:00 - 15:30 | Jean-Michel Couvreur, Nasser Saheb, Grégoire Sutre | An Optimal Automata Approach to LTL Model Checking of Probabilistic Systems |
| 15:30 - 16:00 | Christoph Beierle, Gabriele Kern-Isberner | A Logical Study on Qualitative Default Reasoning with Probabilities |
| 16:00 - 16:30 | Coffee break | |
| Session 5: Linear Logic | ||
| 16:30 - 17:00 | Paola Bruscoli, Alessio Guglielmi | On Structuring Proof Search for First Order Linear Logic |
| 17:00 - 17:30 | Furio Honsell, Marina Lenisa, Rekha Redamalla | Strict Geometry of Interaction Graph Models |
| 17:30 - 18:00 | D. Galmiche, J.M. Notin | Connection-Based Proof Construction in Non-Commutative Logic |
| Session 11 | ||