Tenth Workshop on Automated Reasoning 2003

Abstracts of Contributed Talks

All files are postscript unless stated otherwise.

Invited Speakers

Tom Melham (University of Oxford)
Experience with Practical Formal Verification at an Industrial Scale

Frank Wolter (University of Liverpool)
E-Connections versus Many-Dimensionality

Contributed Talks

David Anderson (University of Portsmouth)
A versatile tree derivation procedure system for multivalent and paraconsistent inference. (pdf)

Quoc Bao Vo, Christoph Benzmueller (Universitaet des Saarlandes), Serge Autexier (DFKI GmbH, Saarbruecken)
Assertion Application in Theorem Proving and Proof Planning

Alexander Bolotov (University of Westminster)
A Clausal Resolution Method for Extended Computation Tree Logic ECTL

Alan Bundy, (University of Edinburgh) Simon Colton (Imperial College London), Sophie Huczynska, (University of Edinburgh) Roy McCasland (University of Edinburgh)
New Directions in Automated Conjecture Making

Liviu Virgil Ciortuz (University of Wales, Aberystwyth),
Generalising Large-Scale Unification Grammars Leads to Improving the Design of an Abstract Machine

Arjeh Cohen, Scott H. Murray (Technische Universiteit Eindhoven) Martin Pollet (Universitat des Saarlandes) Volker Sorge, (University of Birmingham)
Proof Planning some Permutation Group Problems

Anatoli Degtyarev, Kings College, Michael Fisher, Boris Konev (University of Liverpool)
Monodic Temporal Resolution

Louise A. Dennis (University of Nottingham) Ewan Maclean, University of Edinburgh
LambdaClam: A Hierarchical Proof Planning System with Proof Critics

Clare Dixon (University of Liverpool)
Proof Methods for Combinations of Logics

Ann Dobbin (Strathclyde University)
Feedback to aid Formal Specification Error Detection and Correction using Critics

M. Carmen Fernandez Gago, Michael Fisher, Clare Dixon, Wiebe van der Hoek (University of Liverpool)
Logical Verification of Security Protocols

Michael Fisher, Alexei Lisitsa (University of Liverpool)
Deductive Verification of Cache Coherence Protocols

Pierre Flener (Uppsala), Alan M. Frisch (University of York), Brahim Hnich (University College Cork), Chris Jefferson (University of York), Zeynep Kiziltan (Uppsala), Ian Miguel (University of York), Justin Pearson (Uppsala), Toby Walsh (University College Cork)
Breaking Symmetries in Matrix Models: A Brief Overview

Alan Frisch, Ian Miguel (University of York) Toby Walsh (University College Cork)
Refining Abstract Specifications of Constraint Satisfaction Problems

Ian P. Gent (University of St Andrews)
Algebraic Constraint Programming (pdf)

Lilia Georgieva (Heriot-Watt University)
Optimising minimal Herbrand model generation procedures for guarded formulae

Christian Guensel (University of Liverpool)
A tableau based system for deciding EXPSPACE-hard temporalized description logics

Richard Howey, Derek Long (University of Durham)
The Automatic Validation Tool for PDDL2.1

Ullrich Hustadt (University of Liverpool)
SCAN is complete for all Sahlqvist formulae

Derek Long (University of Durham)
Automatic Analysis of Planning Domains(pdf)

Steven Prestwich, Des Higgins, Orla O'Sullivan (University College Cork)
Pseudo-Boolean Multiple Sequence Alignment(pdf)

Tom Ridge (University of Edinburgh)
Formalising a Framework for Distributed Algorithms in Isabelle/HOL

Peter Saffrey (University of Glasgow)
Optimising Communication Structure for Model Checking(pdf)

Renate A. Schmidt (University of Manchester)
Two Proof Systems for Peirce Algebras

Renate A. Schmidt, Dmitry Tishkovsky (University of Manchester)
An Agent Logic Tableau System

Marek Sergot, Rob Craven (Imperial College London)
(C/C+)++: An Action Language for Representing Norms and Institutions

Daniel Sheridan (University of Edinburgh)
Symbol Model Checking for LTL using SNF

Alan Smaill (University of Edinburgh)
Symmetry in Boolean Constraints: Some Complexity Issues

Olga Tveretina, Hans Zantema (TU Eindhoven)
A Resolution-Based Approach for Deciding Equality Logic Formulas

Adrian Williams, Jim Cunningham (Imperial College)
Motivation for a resolution system for a class of prefixed formulas