# 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 #### www.doc.ic.ac.uk/crg/events/ARW07 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 Geoff Sutcliffe, University of Miami Alice Miller, University of Glasgow 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
9:00 - 10:30 | Registration and coffee
10:30 - 12:00 | Abstract 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:30 | Lunch and poster session 1
1:30 - 3:00 | Abstract 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:00 | Coffee and poster session 2
4:00 - 5:00 | Panel session
5:00 - 6:00 | Invited talk 1 (Geoff Sutcliffe) [PDF]
Friday 20th April
9:00 - 10:00 | Coffee
10:00 - 11:30 | Abstract 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:00 | Lunch and poster session 3
1:00 - 2:00 | Invited talk 2 (Alice Miller) [PDF]
2:00 - 3:30 | Abstract 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:30 | Coffee and poster session 4 | 4:30 - 5:00 | ARW business meeting
### 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 Clare Dixon, Chair (University of Liverpool) Jacques Fleuriot Secretary/Treasurer (University of Edinburgh) Brandon Bennett (University of Leeds) Simon Colton (Imperial College London) David Crocker (Escher Technologies) Louise Dennis (University of Liverpool) Roy Dyckhoff (University of St Andrews) Ulle Endriss, (University of Amsterdam) Alan Frisch (University of York) Ullrich Hustadt (University of Liverpool) Mateja Jamnik (Univerity of Cambridge) Tom Melham (University of Oxford) Renate Schmidt (University of Manchester) Volker Sorge (University of Birmingham) ### 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.