Conferences on Intelligent Computer Mathematics - Birmingham 2008
Workshop on Automated Reasoning
Bridging the Gap between Theory and Practice

ARW

Birmingham, UK, 30-31 July 2008

Preliminary Workshop Program

Wednesday, 30 July 2008

Session 1: Invited Talk

09:30-10:30: Andrew Ireland:
Cooperative Reasoning for Automatic Software Verification


10:30-11:00: Coffee Break


Session 2: Short Talks

11:00-11:05: Natasha Alechina, Brian Logan, Nguyen Hoang Nga and Adbur Rakib:
Verification of resource-bounded multi-agent systems

11:05-11:10: Abdelkader Behdanna, Clare Dixon and Michael Fisher:
Analyzing the Behaviour of a Swarm of Foraging Robots Using Temporal Specification and Verification

11:10-11:15: Alessandro Basso, Alexander Bolotov and Vladimir Getov:
Automata-based Formal Specification of Stateful Systems

11:15-11:20: Louise A. Dennis, Rafael H. Bordini, Berndt Farwer and Michael Fisher:
Model-Checking Agent Programming Languages

11:20-11:25: Holger Gast:
Towards Verification by Symbolic Degugging

11:25-11:30: Andrew Ireland, Ewen Maclean and Ianthe Hind:
Proving Functional Properties in Separation Logic


11:30-12:30: Session 3: Poster Session


12:30-14:00: Lunch


Session 4: Panel Discussion

14:00-15:30: It is impossible to automatically generate good representations for reasoning problems


15:30-16:00: Coffee Break


Session 5: Short Talks

16:00-16:05: James P. Bridge, Lawrence C. Paulson and Sean B. Holden:
Applying Machine Learning to Heuristic Selection in an Automatic Theorem Prover

16:05-16:10: Lucas Dixon and Dominic Mulligan:
Dynamic Relational Rippling for HOL

16:10-16:15: Andrew Priddle-Higson, Alan Bundy, Fiona McNeill and Burkhard Schafer:
Ontology Evolution in Law

16:15-16:20: Alan P. Sexton and Volker Sorge:
Reasoning on Abstract Matrix Structures

16:20-16:25: Pedro Torres and Simon Colton:
Toward Meta-Level Theory Formation

16:25-16:30: Lan Zhang, Ullrich Hustadt and Claire Dixon:
A Refined Resolution Calculus for CTL


16:30-17:30: Session 6: Poster Session


19:30-22:00: Dinner


Thursday, 31 July 2008

Session 7: Invited Talk

09:30-10:30: Steve Linton:
Symmetry and Search -- A Survey


10:30-11:00: Coffee Break


Session 8: Short Talks

11:00-11:05: Alexander Bolotov:
Tackling 'Until Induction' in Natural Deduction for PLTL

11:05-11:10: Clare Dixon and John C. McCabe-Danste:
Resolution-Based Proof for a Temporal Logic of Robustness

11:10-11:15: Manfred Kerber:
Normalizations in Propositional Logic

11:15-11:20: Michel Ludwig and Ullrich Hudstadt:
Fair Monodic Temporal Logic Proving

11:20-11:25: Hilver Reker:
A Heuristic for Tableau Reasoning Based on Tree Decompositions of Knowledge Bases

11:25-11:30: Robert Rothenberg:
On the Correspondance between Hypersequent and Labelled Calculi for Intermediate Logics


11:30-12:30: Session 9: Poster Session


12:30-14:00: Lunch


Session 10: Panel Discussion

14:00-15:30: What should make successful research in automated reasoning


15:30-16:00: Coffee Break


16:00-17:00: ARW Committee Meeting