The 12th Workshop on Automated Reasoning
Bridging the gap between theory and practice

29th and 30th July 2005


Day 1 (Friday 29th July)

10:00 Time allocated to mount posters.
10:30 Registration/coffee.
11:00 Invited talk.

Luc Moreau (Electronics and Computer Science, University of Southampton, UK):
"Towards Provenance based Reasoning in E-Science"
12:00 Poster talks (6 speakers talking for 5 minutes each).

William Naylor, Julian Padget, Simone A. Ludwig and Omer F. Rana:
"Semantic Matching and Decomposition of Mathematical Services"

Lin Yang, Alan Bundy, Dave Berry and Conrad Hughes:
"Towards a Bell-Curve Calculus and its Application to e-Science"

Pascal Hitzler and Denny Vrandecic:
"Faster OWL using Split Programs"

Fiona McNeill, Alan Bundy and Chris Walton:
"Enabling Communication between Disparate Agents"

I. Svigkos and A. Bolotov:
"Clausal Resolution in the Framework of Social Agency"

Nivea de C. Ferreira, Michael Fisher and Wiebe van der Hoek:
"A Framework for Uncertain Agents"
12:30 Lunch with posters and demos.
13:45 Invited talk.

Marta Kwiatkowska (School of Computer Science, University of Birmingham, UK):
"Probabilistic Model Checking for the Grid and on the Grid"
14:45 Poster talks (6 speakers talking for 5 minutes each).

Alastair F. Donaldson and Alice Miller:
"Symmetry Reduction for Probabilistic Systems"

Paolo Ballarini, Michael Fisher and Michael Wooldridge:
"Automated Game Analysis via Probabilistic Model Checking"

M. C. Fernandez-Gago, U. Hustadt, C. Dixon, M. Fisher and B. Konev:
"First-Order Theorem Proving in Practice"

Michael Fisher, Boris Konev and Alexei Lisitsa:
"Practical Infinite-State Verification via Temporal Reasoning"

Alan M. Frisch, Chris Jefferson, Bernadette Martinez Hernandez and Ian Miguel:
"The Rules of Constraint Modelling: An Overview"

Ulle Endriss, Markos Hatzitaskos, Paolo Mancarella, Fariba Sadri, Giacomo Terreni and Francesca Toni:
"Refinements of the CIFF Procedure"
15:15 Coffee and posters.
16:30 Panel discussion: "What contribution can automated reasoning make to e-Science?", Chair: Dave Berry, Panelists: Pascal Hitzler, Marta Kwiatkowska and Luc Moreau.
18:00 End of panel discussion.
19:30 Dinner.

Day 2 (Saturday 30th July)

09:00 Invited talk.

Alan M. Frisch (Artificial Intelligence Group, Department of Computer Science, University of York, UK):
"Symmetry and the Generation of Constraint Models"
10:00 Poster talks (6 speakers talking for 5 minutes each).

Manfred Kerber:
"LocModGen - Model Generation by Local Search"

Vladimir Aleksic:
"On Arbitrary Selection Strategies for Superposition"

Juan A. Navarro and Andrei Voronkov:
"Generation of Hard Non-Clausal Random Satisfiability Problems"

Alan P. Sexton and Volker Sorge:
"Abstract Matrices and Constraints"

Alexei Lisitsa and Andrei Nemytykh:
"Verification of Parameterized Systems using Supercompilation"

Andrew Cook and Andrew Ireland:
"Bridging Gaps through Proof Animation"
10:30 Coffee and posters.
11:15 Invited talk.

Mike Gordon (Computer Laboratory, The University of Cambridge):
"Using a Theorem Prover to Implement a Compiler"
12:15 Poster talks (6 speakers talking for 5 minutes each).

Simon Colton, Ferdinand Hoermann, Geoff Sutcliffe and Alison Pease:
"Machine Learning Case Splits for Theorem Proving"

Moa Johansson:
"A Best-First Planner for Rippling"

Andreas Meier and Erica Melis:
"Failure-Reasoning in Multi-Strategy Proof Planning"

Laura I. Meikle and Jacques D. Fleuriot:
"Formal Verification in Computational Geometry"

Sean Wilson and Jacques D. Fleuriot:
"Geometry Explorer: Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs"

Graham Steel:
"Automated Deduction with XOR Constraints"
12:45 Lunch with posters and demos.
14:00 Panel discussion: "The right representation is the key to successful reasoning", Chair: Manfred Kerber, Panelists: Alan Frisch, Ullrich Hustadt and Mateja Jamnik.
15:30 Business meeting.
16:00 End.