| Invited talk |
| 9.30 |
Invited talk: The Quest for the Holy Grail of Agent Verification |
| |
John-Jules Meyer |
|
| Session 1: Workshop (chair: Camilla Schwind) |
| 11.00 |
Cut-free Single-pass Tableaux for the Logic of Common Knowledge |
| |
Pietro Abate, Rajeev Goré, Florian Widmann |
| 11.30 |
Verifying Agent Conformance with Protocols |
| |
Laura Giordano, Alberto Martelli |
| 12.00 |
Towards a Proof Theory for Multi-Agent Logics with Irrevocable Strategies |
| |
Thomas Agotnes, Valentin Goranko, Wojciech Jamroga |
|
| Session 2 (chair: Ugo Moscato) |
| 14.00 |
A tableau method for public announcement logics |
| |
Tiago de Lima, Philippe Balbiani, Hans van Ditmarsch, Andreas Herzig |
| 14.30
|
Tableau systems for logics of subinterval structures over dense orderings |
|
Angelo Montanari, Davide Bresolin, Valentin Goranko, Pietro Sala |
| 15.00
|
KLMLean 2.0: a Theorem Prover for KLM Logics of Nonmonotonic Reasoning |
|
Laura Giordano, Valentina Gliozzi, Gian Luca Pozzato |
|
| Session 3 (chair: Angelo Montanari) |
| 16.00 |
The Neighbourhood of S0.9 and S1 |
|
Roderic Girle |
| 16.30 |
Tableaux with Dynamic Filtration for Layered Modal Logics |
| |
Olivier Gasquet, Bilal Said |
| 17.00 |
On Cut-elimination for Provability Logic GL |
| |
Don Revantha Ramanayake, Rajeev Goré |
| Session 4 (chair: Rajeev Goré) |
| 9.00 |
Invited talk: Nonmonotonic Description Logics - Requirements, Theory, and Implementations |
| |
Piero Bonatti |
| 10.00 |
Differential Dynamic Logic for Verifying Parametric Hybrid Systems |
| |
Andre Platzer |
|
| Session 5 (chair: Didier Galmiche) |
| 11.00 |
Updating Reduced Implicate Tries |
|
Neil Murray, Erik Rosenthal |
| 11.30 |
A Bottom-up Approach to Clausal Tableaux |
| |
Nicolas Peltier |
| 12.00 |
Incremental Closure of Variable Splitting Tableaux |
| |
Christian Mahesh Hansen, Arild Waaler, Roger Antonsen |
|
| Session 6 (chair: Neil Murray) |
| 14.00 |
A Sequent Calculus for Bilattice-Based Logic and its Many-Sorted Representation |
| |
Ekaterina Komendantskaya |
| 14.30 |
Proof Theory for First Order Lukasiewicz Logic |
|
George Metcalfe, Matthias Baaz |
| 15.00 |
A class of theorems in Lukasiewicz logic for benchmarking automated theorem provers |
| |
Robert Rothenberg |
|
| Session 7 (chair: Arild Waaler) |
| 16.00 |
Bounded Model Checking with Description Logic Reasoning |
| |
Shoham Ben-David, Richard Trefler, Grant Weddell |
| 16.30 |
A procedure for description logic ALCFI |
| |
Yu Ding, Volker Haarslev |
| 17.00 |
EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies |
|
Rajeev Goré, Linh Nguyen |
| Session 8 (chair: Marta Cialdea) |
| 9.00 |
Invited talk: Satisfiability Modulo Theories |
| |
Cesare Tinelli |
| 10.00 |
Axiom Pinpointing in General Tableaux |
| |
Franz Baader, Rafael Penaloza |
|
| Session 9 (chair: Roy Dyckhoff) |
| 11.00 |
Tree-Sequent Methods for Subintuitionistic Predicate Logics |
|
Ryo Ishigaki, Kentaro Kikuchi |
| 11.30 |
Improvements to the Tableau Prover PITP |
| |
Guido Fiorino, Alessandro Avellone, Ugo Moscato |
| 12.00 |
A Cut-free Sequent Calculus for Bi-Intuitionistic Logic |
| |
Linda Buisman, Rajeev Goré |