Vol-32 © 2000 for the individual papers by the papers' authors. Copying permitted for private and scientific purposes. Re-publication of material on this page requires permission by the copyright owners.

Automated Reasoning Workshop 2000

Proceedings of the Seventh Workshop on Automated Reasoning,
Bridging the Gap between Theory and Practice,
King's College London, UK, 20-21 July 2000.

Proceedings

The foreword and a list of organisers of the workshop are also available in Postscript format.

You may also download the entire proceedings as a single file, either in compressed Postscript (ps.gz) or Portable Document Format (pdf).

Invited talks

Modal Experiments
Maarten de Rijke

Goal Directed Mechanisms: Proofs, Interpolation and Abduction Procedures
Dov Gabbay

Using Deduction Techniques for Natural Language Understanding
Michael Kohlhase

Contributed abstracts

Resource Guided Concurrent Deduction
Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, and Volker Sorge

The Description Logic Reasoner CICLOP (Version 2.0)
François de Bertrand de Beuvron, Martina Kullmann, David Rudloff, Michael Schlick, and François Rousselot

Automata on Infinite Words and Temporal Logic Normal Forms
Alexander Bolotov

Towards Automating Inductive Proofs for State Monads
Richard J. Boulton

Propositional Temporal Resolution Revised
Anatoli Degtiarev and Michael Fisher

Reasoning in Description Logics with Wellington 1.0 - System Description
Ulrich Endriss

Efficient Control of Temporal Reasoning
M. Carmen Fernández-Gago

Automatic Generation of Implied Constraints: Project Description
Alan M. Frisch and Toby Walsh

Hyperresolution for Guarded Formulae
Lilia Georgieva, Ullrich Hustadt, and Renate A. Schmidt

Forward and Backward Chaining in Linear Logic
James Harland, David Pym, and Michael Winikoff

Congruence Classes with Logic Variables
Joe Hurd

Practical Proof Methods for Combined Modal and Temporal Logics
Ullrich Hustadt

The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable
Konstantin Korovin and Andrei Voronkov

Automatic Generation of Concurrent Provers
Raul H. C. Lopes

Finite Model Building for Propositional Gödel-Logics as an Example for Projective Logics
Markus Moschner

Theorem Proving for Temporal Logics of Knowledge or Belief
Cláudia Nalon

Application of Simplification Theories
Mauricio Osorio, Juan Carlos Nieves, and Gabriel Cervantes

A Deductive Decision Procedure for a Restricted FTL
Regimantas Pliuskevicius

Run-time Optimisations for Reasoning with Intensional Logics
Allan Ramsay

System Description: Vampire 1.0
Alexandre Riazanov and Andrei Voronkov

A Decision Procedure for Term Algebras with Queues
Tatiana Rybina and Andrei Voronkov

Description Logics and Knowledge Discovery of Data
Stefan Schlobach

Deciding Fluted Logic with Resolution
Renate A. Schmidt