| Session 1 | ||
| 10:00 - 10:30 | J. Siekmann, C. Benzmüller, A. Fiedler, A. Meier, and M. Pollet | Proof Development With Omega: sqrt{2} is Irrational |
| 10:30 - 11:00 | Claudio Castellini and Alan Smaill | Proof Planning for Feature Interactions: a Preliminary Report |
| 11:00 - 11:30 | Julian Richardson | A Semantics for Proof Plans with Applications to Interactive Proof Planning |
| Coffee break | ||
| Session 2 | ||
| 12:00 - 12:30 | AK McIver and CC Morgan | Games, Probability and the Quantitative mu-Calculus |
| 12:30 - 13:00 | Pascal Fontaine and E. Pascal Gribomont | Using BDDs with Combinations of Theories |
| Lunch | ||
| Session 3: invited talk | ||
| 14:30 - 15:30 | Kostic Sagonas | Tabling in Logic Programming and its Implementations |
| Coffee break | ||
| Session 4 | ||
| 16:00 - 16:30 | James Brotherston, Anatoli Degtyarev, Michael Fisher, and Alexei Lisitsa | Searching for Invariants Using Temporal Resolution |
| 16:30 - 17:00 | Temur Kutsia | Theorem Proving with Sequence Variables and Flexible Arity Symbols |
| 17:00 - 17:30 | Sergio Tessaris and Ian Horrocks | Abox Satisfiability Reduced to Terminological Reasoning in Expressive Description Logics |
| 17:30 - 18:00 | Fabio Grandi | On Expressive Description Logics with Composition of Roles in Number Restrictions |
| 19:00 Conference dinner | ||
| Session 5 | ||
| 9:30 - 10:00 | Jose Espirito Santo | An Isomorphism Between a Fragment of Sequent Calculus and an Extension of Natural Deduction |
| 10:00 - 10:30 | Stefan Edelkamp and Peter Leven | Directed Automated Theorem Proving |
| 10:30 - 11:00 | Lutz Strassburger | A Local System for Linear Logic |
| Coffee break | ||
| Session 6 | ||
| 11:30 - 12:00 | Martin Strecker | Investigating Type-Certifying Compilation with Isabelle |
| 12:00 - 12:30 | Don Syme and Andrew D. Gordon | Automating Type Soundness Proofs via Decision Procedures and Guided Reductions |
| 12:30 - 13:00 | M. Alpuente, S. Escobar, B. Gramlich, and S. Lucas | Improving On-Demand Strategy Annotations |
| Lunch | ||
| Session 7: invited talk | ||
| 14:30 - 15:30 | Christian Fermüller | Parallel Dialogue Games for Intermediate Logics |
| Coffee break | ||
| Session 8 | ||
| 16:00 - 16:30 | Norbert Preining | Gödel Logics and Cantor-Bendixon Analysis |
| 16:30 - 17:00 | K. R. Apt and C. F. M. Vermeulen | First-Order Logic as a Constraint Programming Language |
| 17:00 - 17:30 | Joachim Niehren and Mateu Villaret | Parallelism and Tree Regular Constraints |
| 17:30 - 18:00 | Arnold Beckmann | A Note on Universal Measures for Weak Implicit Computational Complexity |
If weather permits, we will visit the village Kasbegi driving along the famous "Georgian Military Road" constructed in the 19th century. This gives us the possibility to see the awesome mountain range of High Caucasus from short distance. We will visit the famous church on the slopes of Mount Kasbegi, the king of Caucasus (second highest mountain after Elbrus). On the way we will have the opportunity to visit several castles and churches, including the churches of Mxeta, the ancient capital of Georgia.
The excursion will be followed by a barbecue until late in the night.
| Session 9 | ||
| 9:30 - 10:00 | Benedikt Bollig, Martin Leucker, and Philipp Lucas | Extending Compositional Message Sequence Graphs |
| 10:00 - 10:30 | Gilles Dowek, Therese Hardin and Clause Kirchner | Binding Logic: Proofs and Models |
| 10:30 - 11:00 | Mehdi Dastani and Leendert van der Torre | An Extension of BDI-CTL with Functional Dependencies and Components |
| Coffee break | ||
| Session 10 | ||
| 11:30 - 12:00 | Serge Autexier and Dieter Hutter | Maintenance of Formal Software Developments by Stratified Verification |
| 12:00 - 12:30 | Alessio Guglielmi and Lutz Strassburger | A Non-Commutative Extension of MELL |
| 12:30 - 13:00 | Mauro Ferrari, Camillo Fiorentini, and Guido Fiorino | On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics |
| Lunch | ||
| Session 11 | ||
| 14:30 - 15:00 | Gianluigi Greco, Sergio Greco, Irina Trubtsyna, and Ester Zumpano | Query Optimization of Disjunctive Databases with Constraints Through Binding Propagation |
| 15:00 - 15:30 | Claudio Vaucheret, Sergio Guadarrama, and Susana Munoz | Fuzzy Prolog: a Simple General Implementation Using CLP(R) |
| 15:30 - 16:00 | Orna Kupferman, Nir Piterman, and Moshe Y. Vardi | Pushdown Specifications |
The Friday programme will consist of:
running in parallel. The workshop programme is available at the workshop programme page The poster session programme is given below and scheduled so as not to interfere with the invited talks of the workshop.
There will be an overview excursion of Tbilisi followed by a dinner in a (nice) restaurant in Tbilisi until very late. The excursion will start at 17:00, immediately after the last workshop talk.
| Session A | ||
| 10:35 - 10:40 | Tanel Tammet | Efficient finite model building using the Mace algorithm and non-ground splitting |
| 10:40 - 10:45 | Anna Romina | TBA |
| 10:45 - 10:50 | Konstantin Pkhakadze and M. Ivanishvili | Towards the Strong Formal Logic Understanding of the Word Based on the Natural Georgian Language System |
| 10:50 - 10:55 | Khimuri Rukhaia and Lali Tibua | A Problem in Mechanical Theorem Proving |
| Coffee break | ||
| 11:15 - 11:20 | Juan Heguiabehere | Pre- and Postcondition Reasoning in Dynamic First Order Logic |
| 11:20 - 11:25 | Alessandro Avellone, Guido Fiorino, Ugo Moscato. | A new O(n log n)-SPACE decision procedure for propositional intuitionistic logic |
| 11:25 - 12:30 | Posters | |