Workshop on Automated Reasoning
Bridging the Gap between Theory and Practice


Automated Reasoning Workshop 2007

19th-20th April 2007

Department of Computing

Imperial College, London

Continuing the highly successful series of Workshops on Automated Reasoning, this event will provide an informal forum for the automated reasoning community. The ARW workshop series aims to bring together researchers from all areas of automated reasoning in order to foster links and facilitate cross-fertilisation of ideas among researchers from various disciplines; among researchers from academia, industry and government; and between theoreticians and practitioners.

Details of the ARW organisation and of previous ARW events can be found at the ARW website.

TPTP Tea Party

Geoff Sutcliffe will be holding the annual TPTP tea party at Imperial following the ARW workshop. Please see:

for more details.


Registration for the workshop is now open. Please fill in the form below and fax it to:
Dr. Simon Colton, Imperial College, London,
using this number: +44 (0)20 7581 8024.
Registration form (Word Document)      Registration form (PDF)


Unfortunately, Imperial doesn't rent out its student rooms during the Easter break. However, Imperial does have an accommodation link office, and if you book through them, they can get discounted rates in hotels around the South Kensington area. Having said that, rooms in London are still expensive - sorry about that.

The website to look at is here:

The cheapest hotel seems to be Wellington Hotel, which is a little distance away, but not too bad (it is an ex-hall of residence). Their price is 40 pounds per night. The next best is the Norfolk Towers, at 63 pounds per night.

Invited Speakers

Abstract for Geoff's talk:

This talk describes the design, implementation, and testing of a system for selecting necessary axioms from a large set also containing superfluous axioms, to obtain a proof of a conjecture. The selection is determined by semantics of the axioms and conjecture, ordered 40 per night. The next best seems to be The Norfolk Towers, at heuristically by a syntactic relevance measure. The system is able to solve many problems that cannot be solved alone by the underlying automated reasoning system.

Abstract for Alice's talk:

Model checking is an established technique for checking the reliability of software-controlled systems and constitutes one of the leading applications of logic to Computer Science. This automatic technique involves the construction of a model of a system over which properties are checked. One of the major problems with model checking is the (so-called) state-space explosion problem -- where models become too large to feasibly-- -- check. A popular technique for combatting state-space explosion is symmetry reduction. In this talk I introduce a variety of model checkers and give an introduction to symmetry reduction methods, and their implementations.


Thursday 19th April

9:00 - 10:30Registration and coffee
10:30 - 12:00Abstract session 1 (10 minute presentations)
[Roughly] Higher Order Logics and Languages
Bolotov/Grigoriev/Shangin   Craven/Sergot   Dennis/Bordini/Fisher/Farwer   Dixon/Fisher/Konev
Schmidt/Tishkovsky   Stankovic/Krdzavac/Devedzic   Zhang/Dixon/Hustadt  
12:00 - 1:30Lunch and poster session 1
1:30 - 3:00Abstract session 2 (10 minute presentations)
[Roughly] Verification and other Applications
Basso/Bolotov   Bundy   Gow/Cairns   Hu/Lawford/Wassyng
Kowalski   Li/Schmidt   Mehta  
3:00 - 4:00Coffee and poster session 2
4:00 - 5:00Panel session
5:00 - 6:00Invited talk 1 (Geoff Sutcliffe) [PDF]

Friday 20th April

9:00 - 10:00Coffee
10:00 - 11:30Abstract session 3 (10 minute presentations)
[Roughly] Resolution and other Reasoning Techniques
Aleksic   Amjad   Benzmuller/Paulson/Thiess/Fietzke
Johansson/Dixon/Bundy   Kahramanogullari   Ludwig   Robinson  
11:30 - 1:00Lunch and poster session 3
1:00 - 2:00Invited talk 2 (Alice Miller) [PDF]
2:00 - 3:30Abstract session 4 (10 minute presentations)
[Roughly] Combination/Integration/Hybridization
Aspinall/Luth   Broda/Russo   Charlton/Huth
Charnley/Colton   Navarro-Perez/Voronkov   Carette/Farmer/Sorge   Torres/Colton  
3:30 - 4:30Coffee and poster session 4 4:30 - 5:00ARW business meeting


We are very grateful for sponsorship from the SymNet Network, details of which can be found here:


Extended Abstracts

We will be publishing a timetable soon. Authors: please let Simon Colton know of any timetabling restriction you have (

Forms of factoring in paramodulation-based calculi
Vladimir Aleksic

Compressing propositional refutations using subsumption
Hasan Amjad

Proof tool integration with Proof General
David Aspinall and Christoph Luth

Towards automated verification of grid component model
Alessandra Basso and Alexander Bolotov

The LEO-II Project
Christoph Benzmuller, Larry Paulson, Frank Theiss and Arnaud Fietzke

Automating Natural Deduction for Temporal Logic
Alexander Bolotov, Oleg Grigoriev and Vasilyi Shangin

A tableau compiled labelled deductive system for hybrid logic
Krysia Broda and Alessandra Russo

Towards a theory of ontology repair (or truthfulness considered harmful)
Alan Bundy

A rational reconstruction of a system for experimental mathematics
Jacques Carette, William Farmer and Volker Sorge

Cleanly combining specialised program analysers
Nathaniel Charlton and Michael Huth

Prediction using machine learned constraint satisfaction programs
John Charnley and Simon Colton

The Language EC+
Robert Craven and Marek Sergot

A common semantic basis for BDI languages
Louise Dennis, Rafael Bordini, Michael Fisher and Berndt Farwer

Tractable temporal reasoning
Clare Dixon, Michael Fisher and Boris Konev

A digital library based on Mizar
Jeremy Gow and Paul Cairns

Proof critics for IsaPlanner
Moa Johansson, Lucas Dixon and Alan Bundy

Interaction and depth against nondeterminism in proof search
Ozan Kahramanogullari

Computational Logic as a Cognitive Model
Bob Kowalski

Formal verification of implementability of timing requirements
Mark Lawford, Xiayong Hu and Alan Wassung

Dynamic backtracking for modal logics
Zhen Li and Renate Schmidt

Extensions of the Knuth-Bendix ordering with LPO-like properties
Michel Ludwig

Supporting proof in a reactive development environment
Farhad Mehta

Encodings of bounded LTL model checking in effectively propositional logic
Juan Navarro-Perez and Andrei Voronkov

Using resolution to generate natural proofs
David Robinson

Analysis of blocking mechanisms for description logics
Renate Schmidt and Dmitry Tishkovsky

A universal GUI for theorem provers
Bosko Stankovic, Nenad Krdzavac and Vladan Devedzic

SRASS - a semantic relevance axiom selection system
Geoff Sutcliffe

Proving producibility of concepts
Pedro Torres and Simon Colton

Implementing tractable temporal logics
Lan Zhang, Clare Dixon and Ulrich Hustadt


Each workshop attendee will be allocated a 10 minute slot for a short talk to introduce their research. Each attendee will also be allocated space in a poster session, where they can further present and discuss their work. Please prepare posters for the event.


We have organised lunches for both days of the workshop.

The workshop meal will be in the Med Kitchen, South Kensington.
It is very close to the Department, with a map here:

Med kitchen map

The restaurant will offer a 3 course menu followed by coffee or tea. Each course features a choice from 4 dishes including a vegetarian option. The cost is 22.95 excluding drinks and gratuity.


The workshop is being organised by the Combined Reasoning Group at Imperial.

Program Committee

Travel details

Details of how to get to the department of computing can be found here:
Huxley Building - Travel Details


Please contact Simon Colton ( if you have any queries about the 2007 Automated Reasoning Workshop.