9:00- 9:45 |
Invited Talk |
A Tale of Two Logics, Three Systems, Four Languages, and Fifteen Years |
Peter F. Patel-Schneider |
9:45-10:30 |
Invited Talk |
|
Alessandro Cimatti |
10:30-11:00 |
Coffee |
|
|
11:00-11:20 |
|
Designing an efficient library for propositional reasoning and beyond |
E. Giunchiglia, M. Narizzano, A. Tacchella, M. Vardi |
11:20-11:40 |
|
A Subsumption-Aided Caching Technique |
Jens Happe |
11:40-12:00 |
|
Combining Tableaux and Algebraic Decision Procedures for Dealing with
Qualified Number Restrictions in Description Logics |
Volker Haarslev, Martina Timmann, Ralf Moeller |
12:00-12:20 |
|
Temporal Logic Theorem Proving and its Application to the Feature Interaction
Problem |
Amy Felty |
12:20-12:40 |
|
Tactical Theorem proving in First order Temporal Logics |
Claudio Castellini, Alan Smaill |
12:30-14:00 |
Lunch |
|
|
14:00-14:45 |
Invited Talk |
Evaluating General Purpose Automated Theorem Proving Systems |
Geoff Sutcliffe |
14:45-15:30 |
Invited Talk |
|
Gila Kamhi |
15:30-16:00 |
Coffee |
|
|
16:00-16:20 |
|
The Random Modal QBF Test Set |
Juan Heguiabehere and Maarten de Rijke |
16:20-16:40 |
|
Improving the Generation of Random Modal Formulae for testing decision
procedures |
Peter Patel-Schneider, Roberto Sebastiani |
16:40-17:00 |
|
Formulae which Highlight differences between Temporal Logic and Dynamic
Logic Provers |
Ullrich Hustadt, Renate Schmidt |
17:00-17:20 |
|
Generating Symbolic Model Checking benchmarks by reduction from QBF |
F. Donini, P. Liberatore, F. Massacci, M. Schaerf |
17:20-18:00 |
|
Open Discussion |
Initiators: E. Giunchiglia, F. Massacci |