PROGRAM


Printable version here.






































Workshops
Session 1

Tableaux S1
FroCoS S1, joint with Tableaux
Joint FroCoS + Tableaux
FroCoS starts at 9:30


Tobias Nipkow
Lawrence C. Paulson
Stéphane Demri
FroCoS S7


+ 1 regular paper
+ 1 regular paper
+ 1 regular paper
Konstantin Korovin

Coffee
Coffee
Coffee
Coffee
Coffee

Workshops
Session 2

Tableaux S2
Tableaux FroCoS S2
Tableaux S7 FroCoS S4
FroCoS S8


 
Tutorials  
   
 


 
   
   
 





until 13:00

FroCoS Business Meeting


Lunch
Lunch
Lunch
Lunch
Lunch













Workshops
Session 3

Tableaux S3
Tableaux S5, joint with FroCoS
FroCoS S5, joint with Tableaux
FroCoS S9


 
Sara Negri
Joël Ouaknine
 


 
+ 1 regular paper
+ 1 regular paper
 

Coffee
Coffee
Coffee
Coffee
Coffee

Workshops
Session 4

Tableaux S4
Tableaux S6 FroCoS S3
Tableaux S8 FroCoS S6



until 17:00
   
   





   
   






Tableaux Business Meeting























Tableaux reception
FroCoS reception
FroCoS + Tableaux Dinner






starting 18:15
starting 19:00
starting 19:30


Color code: FroCoS event
Tableaux event
FroCoS + Tableaux event


Monday, 16 September 2013


08:45 - 09:30 Registration
09:15 - 17:30 Two workshops of four sessions each in rooms A006 and B013.
Please visit the workshops page.


Tuesday, 17 September 2013


08:30 - 08:55 Registration
08:55 - 09:00 Welcome
Tableaux Session 1 Chair: Dominique Larchey-Wendling
09:00 - 10:00 Keynote speaker: Tobias Nipkow (and Andrei Popescu)
A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
Joint work with Maximilian Haslbeck
10:00 - 10:30 Hendrik Tews
Formalizing Cut Elimination of Coalgebraic Logics in Coq
10:30 - 11:00 Coffee break
Tableaux Session 2 Chair: Neil Murray
11:00 - 11:30 Andreas Bauer, Peter Baumgartner, Martin Diller and Michael Norrish
Tableaux for Verification of Data-Centric Processes
11:30 - 12:00 Tim French, John McCabe-Dansted and Mark Reynolds
Model Checking for Compositional Models of General Linear Time
12:00 - 12:30 Nicolas Peltier
Schemata of formulae in the theory of arrays
12:30 - 14:00 Lunch break
Tableaux Session 3 Chair: Nicolas Peltier
14:00 - 14:30 Ulrich Furbach and Claudia Schon
Semantically Guided Evolution of SHI ABoxes
14:30 - 15:00 Mohammad Khodadadi, Renate A. Schmidt and Dmitry Tishkovsky
A Refined Tableau calculus with Controlled Blocking for the Description Logic SHOI
15:00 - 15:30 Ming Zuo and Volker Haarslev
Intelligent Tableaux Algorithm for DL Reasoning
15:30 - 16:00 Coffee break
Tableaux Session 4 Chair: Jens Otten
16:00 - 16:30 Christoph Röthlisberger
TAFA - A Tool for Admissibility in Finite Algebras
16:30 - 17:00 Davide Bresolin, Dario Della Monica, Angelo Montanari and Guido Sciavicco
A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: an Implementation
Social Program
18:15 - Tableaux reception
Musée Aquarium de Nancy, jardin D. A. Godron (11-13, Rue Godron, Nancy)
Short presentation, free visit followed by reception
A map of the trip to the reception site


Wednesday, 18 September 2013


FroCoS Session 1 Chair: Pascal Fontaine
09:00 - 10:00 Keynote speaker: Lawrence C. Paulson
MetiTarski's Menagerie of Cooperating Systems
10:00 - 10:30
FroCoS paper
Abdelkader Kersani and Nicolas Peltier
Combining Superposition and Induction: A Practical Realization
10:30 - 11:00 Coffee break
Tableaux Tutorials
11:00 - 13:00
Room A006
Sorin Stratulat
Noetherian Induction for First-Order Reasoning
11:00 - 13:00
Room B013
Dmitry Tishkovsky and Renate A. Schmidt
Generating tableau provers using MetTeL2
13:00 - 14:00 Lunch break
Tableaux Session 5 Chair: Dale Miller
14:00 - 15:00 Keynote speaker: Sara Negri
On the duality of proofs and countermodels in labelled sequent calculi
15:00 - 15:30
Tableaux paper
Zhe Hou, Alwen Tiu and Rajeev Gore
A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
15:30 - 16:00 Coffee break
Tableaux Session 6 Chair: Rajeev Goré
16:00 - 16:30 Stefan Hetzl, Tomer Libal, Martin Riener and Mikheil Rukhaia
Understanding Resolution Proofs through Herbrand's Theorem
16:30 - 17:00 Bjoern Lellmann and Dirk Pattinson
Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5
17:00 - 17:30 Hidenori Kurokawa
Prefixed tableau systems for logic of proofs and provability
17:30 - 18:00 Tableaux Business Meeting
Social Program
19:00 - FroCoS reception
Musée Lorrain (64, Grande Rue, Nancy)
Short visit followed by reception


Thursday, 19 September 2013


Joint Session Chair: Silvio Ghilardi
09:00 - 10:00 Keynote speaker: Stéphane Demri
Witness Runs for Counter Machines Joint work with Clark Barrett and Morgan Deters
10:00 - 10:30
Tableaux paper
Joseph Boudou and Bruno Woltzenlogel Paleo
Compression of Propositional Resolution Proofs by Lowering Subproofs
10:30 - 11:00 Coffee break
Tableaux Session 7 Chair: Arild Waaler
11:00 - 11:30 Agata Ciabattoni, Paolo Maffezioli and Lara Spendier
Hypersequent and Labelled Calculi for Intermediate Logics
11:30 - 12:00 Mauro Ferrari, Camillo Fiorentini and Guido Fiorino
A terminating evaluation-driven variant of G3i
12:00 - 12:30 Stéphane Graham-Lengrand
Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
12:30 - 14:00 Lunch break
FroCoS Session 5 Chair: Silvio Ranise
14:00 - 15:00 Keynote speaker: Joël Ouaknine
Specification and Verification of Linear Dynamical Systems: Advances and Challenges
15:00 - 15:30
FroCoS paper
Matthias Horbach and Viorica Sofronie-Stokkermans
Obtaining Finite Local Theory Axiomatizations via Saturation
15:30 - 16:00 Coffee break
Tableaux Session 8 Chair: Hans van Ditmarsch
16:00 - 16:30 Nick Bezhanishvili and Silvio Ghilardi
Bounded proofs and step frames
16:30 - 17:00 Carlos Areces and Ezequiel Orbe
Dealing with Symmetries in Modal Tableaux
17:00 - 17:30 Amélie David
TATL: Implementation of an ATL Tableau-Based Decision Procedure
Social Program
19:30 - Conference dinner (2, Place Stanislas, Nancy)
Grand Hôtel de la Reine