Automated Reasoning Workshop

19th - 20th April 2007

Department of Computing, Imperial College, London

http://www.doc.ic.ac.uk/crg/events/ARW07

-------------------------------------------------
CALL FOR PARTICIPATION
-------------------------------------------------

The 2007 automated reasoning workshop is the latest in a long series
of successful workshops which aim to provide an informal forum for the
automated reasoning community to discuss recent work, new ideas and
current trends. It 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.

Please find below details of this year's workshop:

-------------
INVITED TALKS
-------------

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
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.

------------------------------------------
EXTENDED ABSTRACTS WHICH WILL BE PRESENTED
------------------------------------------

We have a very broad and interesting selection of extended abstracts
which will be presented this year. Each extended abstract will be
discussed both with a short presentation and in a poster session.

Forms of factoring in paramodulation-based calculi
Vladimir Aleksic

Compressing propositional refutations using subsumption
Hasan Amjad

Proof tool integration with proof general
David Asipinall 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

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

---------------------------------
PLEASE COME ALONG TO THE WORKSHOP
---------------------------------

Registration for the workshop has recently been opened. For details of
how to register, please see the workshop web page here:

http://www.doc.ic.ac.uk/crg/events/ARW07

---------------
CONTACT DETAILS
---------------

If you have any questions about the workshop, please do not hesitate to
contact the workshop organiser: Simon Colton (sgc@doc.ic.ac.uk).