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