Workshop on Automated Reasoning
Bridging the Gap between Theory and Practice
Automated Reasoning Workshop 2009
(21st-22nd April 2009, Department of Computer Science, University of Liverpool)
All session take place in the Second floor seminar room, Ashton Building, unless
otherwise indicated.
Tuesday, 21 April 2009
10:00 Registration / Coffee
(Ground floor seminar room, Ashton Building)
Poster set up opportunity (for first poster session)
(Second floor meeting room, Ashton Building)
10:50 Welcome
11:00 Short Talks (approximately five minutes each)
* S. Konur and M. Fisher:
Verification of Pervasive Systems
* M. Horridge, B. Paris, and U. Sattler:
Computing Explanations for Entailments in Description Logic Based Ontologies
* Q.-a. Mahesar and V. Sorge:
Classification of Quasigroup-structures with respect to their Cryptographic Properties
* R. A. Schmidt:
The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction
* L. Zhang, U. Hustadt, and C. Dixon:
CTL-RP: A Computational Tree Logic Resolution Prover
11:30 Posters and Coffee
(Second floor meeting room, Ashton Building)
12:30 Lunch
(Ground floor seminar room, Ashton Building)
13:30 Invited Talk
Stefan Szeider (Durham University):
Finding Hidden Structures in Reasoning Problems
14:30 Short Talks (approximately five minutes each)
* A. Basso, A. Bolotov, and V. Getov:
State-Based Behavior Specification for GCM Systems
* M. Ludwig and U. Hustadt:
TSPASS - a Fair Monodic Temporal Logic Prover
* C. Power and A. Miller:
Symmetry Reduction of Partially Symmetric Systems
* R. Ramezani and S. Colton:
Solving Mutilated Problems
* R. A. Schmidt and D. Tishkovsky:
Synthesising Tableau Decision Procedures
* G. Stapleton, M. Jamnik, and J. Masthoff:
On the Readability of Diagrammatic Proofs
15:00 Posters and Coffee
(Second floor meeting room, Ashton Building)
16:00 Panel Discussion
Challenges in Applications of Automated Reasoning
17:00 (Business Meeting of the Organising Committee)
19:30 Conference Dinner
Wednesday, 22 April 2009
10:00 Invited talk
Konstantin Korovin (University of Manchester):
Instantiation-Based Automated Reasoning For First-Order Logic
11:00 Short Talks (approximately five minutes each)
* L. A. Dennis and L. Dixon:
Adapting Piecewise Fertilisation to Reason about Hypotheses
* B. Konev, C. Dixon, and M. Fisher:
"Exactly One" Epistemic Logic
* S. H. Ripon and A. Miller:
Semantic Embedding of Promela-Lite in PV
* C. Sticksel:
Efficient Ground Satisfiability Solving in an Instantiation-based Method for First-order Theorem Proving
* P. Torres and S. Colton:
First-Order Logic Concept Symmetry for Theory Formation
11:30 Posters and Coffee
(Second floor meeting room, Ashton Building)
12:30 Lunch
(Waterhouse Cafe, Victoria Building)
14:00 Panel Discussion
Challenges in Advancing Automated Reasoning
15:00 Short Talks (approximately five minutes each)
* A. Bolotov and O. Grigoriev:
Natural Deduction Calculus for Quantified Propositional Linear-time Temporal Logic (QPTL)
* S. Feng:
Combining Generalisation Into Instantiation Based Reasoning In EPR
* S. Konur (presented by S. Schewe):
A Decidable Approach to Real-time System Specification
* M. Webster, L. Dennis, and M. Fisher:
Model-Checking Auctions, Coalitions and Trust
* M. Ridsdale, M. Jamnik, N. Benton, and J. Berdine:
Diagrammatic Reasoning for Software Verification
15:30 Posters and Coffee
(Second floor meeting room, Ashton Building)
16:30 Close