CONFERENCE PROGRAM
All talks take place in room B5 unless otherwise noted.
Please click here for a printer friendly version of the program.
You might also be interested in the proceedings.
Monday 4 July
FTP 2011 will take place in room B77 (see details)
GSB 2011 will take place in room B78 (see details)
| | FTP | GSB |
| 09.15-10.00 | Registration |
| 10.00-11.00 | Monitoring First-order Temporal Properties | Nested Sequents and Prefixed Tableaus |
| | Felix Klaedtke (Invited Talk) | Melvin Fitting (Invited Talk) |
| 11.00-11.30 | Coffee Break |
| 11.30-12.00 | Implementing and Evaluating Theorem Provers for First-Order Modal Logics | Some Remarks on Nested Sequent Systems for Modal Logics |
| | Thomas Raths and Jens Otten | Lutz Straßburger |
| 12.00-11.30 | Generating Schemata of Resolution Proofs | Constructive Realization in Justfication Logics via Nested Sequents |
| | Vincent Aravantinos and Nicolas Peltier | Remo Goetschi |
| | Incremental Variable Splitting | Sequent Calculus for Justifications |
| | Christian Mahesh Hansen, Martin Giese, Arild Waaler and Roger Antonsen | Yury Savateev |
| 13.00-14.30 | Lunch |
| 14.30-15.00 | Modular Termination and Combinability for Superposition Modulo Counter Arithmetic | A Symmetric Natural Deduction |
| | Christophe Ringeissen and Valerio Senni | Michel Parigot |
| 15.00-15.30 | QMaxSAT version 0.3 & 0.4 | |
| | Xuanye An, Miyuki Koshimura, Hiroshi Fujita and Ryuzo Hasegawa | |
| 15.30-16.00 | Unification in a Theory of Blind Signatures | A Tentative Atomic Calculus for Natural Deduction |
| | Serdar Erbatur, Christopher Lynch and Paliath Narendran | Tom Gundersen |
| 16.00-16.30 | Coffee Break |
| 16.30-17.00 | FTP Business Meeting | On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics |
| | | Alwen Tiu |
| 17.00-17.30 | | Definite and Indefinite Descriptions |
| | | Norbert Gratzl |
| 20.00 | Workshop Dinner |
Tuesday 5 July
| 09.00-09.30 | Registration |
| 09.30-10.30 | On Interpolation in Decision Procedures |
| | Maria Paola Bonacina (Invited Talk) |
| 10.30-11.00 | Coffee Break |
Session 1 (Chair: Neil Murray)
| 11.00-11.30 | The Modal mu-Calculus Caught Off Guard |
| | Oliver Friedmann and Martin Lange |
| 11.30-12.00 | Hybrid and First-order Complete Extensions of CARET |
| | Laura Bozzelli and Ruggero Lanotte |
| 12.00-12.30 | Correctness and Worst-case Optimality of Pratt-style Decision Procedures for Modal and Hybrid Logics |
| | Mark Kaminski, Thomas Schneider and Gert Smolka |
| 12.30-13.00 | A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders |
| | Serenalla Cerito and Marta Cialdea Mayer |
| 13.00-14.30 | Lunch |
Session 2 (Chair: Nicola Olivetti)
Wednesday 6 July
| 09.30-11.00 | Tutorials |
| | Tableaux(-like) Methods for the Satisfiability Problems of Temporal Logics (B77) |
| | Martin Lange |
| | Introduction to Proof Nets (B78) |
| | Lutz Straßburger |
| 11.00-11.30 | Coffee Break |
| 11.30-13.00 | Tutorials |
| | Tableaux(-like) Methods for the Satisfiability Problems of Temporal Logics (B77) |
| | Martin Lange |
| | Introduction to Proof Nets (B78) |
| | Lutz Straßburger |
| 13.00-14.30 | Lunch |
Session 3 (Chair: Rajeev Gore)
| 14.30-15.00 | A Non-Clausal Connection Calculus |
| | Jens Otten |
| 15.00-15.30 | Schemata of SMT problems |
| | Vincent Aravantinos and Nicolas Peltier |
| 15.30-16.00 | CsymLean: a Theorem Prover for the Logic CSL over Symmetric Minspaces |
| | Regis Alenda and Nicola Olivetti |
| 16.00-16.30 | Coffee Break |
Session 4 (Chair: Martin Giese)
| 16.30-16.50 | A Dynamic Programming Algorithm for Prime Implicates |
| | Andrew Matusiewicz |
| 16.50-17.10 | Dialogue Games for Classical Logic |
| | Jesse Alama, Sara L. Uckelman and Aleks Knoks |
| 17.10-18.30 | Tableaux Business Meeting |
Thursday 7 July
| 09.30-10.30 | Proof Theory and Algebra in Substructural Logics |
| | Kazushige Terui (Invited Talk) |
| 10.30-11.00 | Coffee Break |
Session 5 (Chair: Arnon Avron)
| 11.00-11.30 | Cut Elimination for Modal Logics with Shallow Axioms |
| | Bjoern Lellmann and Dirk Pattinson |
| 11.30-12.00 | Craig Interpolation in Displayable Logics |
| | James Brotherston and Rajeev Gore |
| 12.00-12.30 | On the Proof Complexity of Cut-Free Bounded Deep Inference |
| | Anupam Das |
| 12.30-13.00 | A Tableau Calculus for a Nonmonotonic Extension of EL\bot |
| | Laura Giordano, Valentina Gliozzi, Nicola Olivetti and Gian Luca Pozzato |
| 13.00-14.30 | Lunch |
| 14.30-19.30 | Excursion |
| 19.30-22.30 | Dinner at Kornhauskeller Restaurant |
Friday 8 July
| 09.30-10.30 | First-order Tableaux in Applications |
| | Ulrich Furbach (Invited Talk) |
| 10.30-11.00 | Coffee Break |
Session 6 (Chair: Jens Otten)
| 11.00-11.30 | MaLeCoP: A Machine Learning Connection Prover |
| | Josef Urban, Jiri Vyskocil and Petr Stepanek |
| 11.30-12.00 | MetTeL: A Tableau Prover with Logic-Independent Inference Engine |
| | Dmitry Tishkovsky, Renate A. Schmidt and Mohammed Khodadidi |
| 12.00-12.30 | A Conditional Constructive Logic for Access Control and its Sequent Calculus |
| | Valerio Genevose, Laura Giordano, Valentina Gliozzi and Gian Luca Pozzato |
| 12.30-13.00 | Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders |
| | Davide Bresolin, Angelo Montanari, Pietro Sala and Guido Sciavicco |
| 13.00-14.30 | Lunch |