Automated Reasoning Workshop 2007
19th-20th April 2007
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:
TPTPTP
for more details.
Registration
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)
Accommodation
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:
http://www.imperial-accommodationlink.com
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.
Timetable
Thursday 19th April
Friday 20th April
Sponsorship
We are very grateful for sponsorship from the SymNet Network, details
of which can be found here:
SymNet
Extended Abstracts
We will be publishing a timetable soon. Authors: please let Simon Colton
know of any timetabling restriction you have (sgc@doc.ic.ac.uk).
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
Presentations
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.
Meals
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.
Organisers
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
Contact
Please contact Simon Colton (sgc@doc.ic.ac.uk)
if you have any queries about the 2007 Automated Reasoning
Workshop.
|