Automated Reasoning Workshop 2000

Thursday, 20 July 2000

Morning  Chair: Hans Jürgen Ohlbach
9.00 1B27 Registration desk open

10.00 1B06 Session I: Temporal Reasoning, Model Building • Anatoli Degtiarev and Michael Fisher

• Propositional Temporal Resolution Revised

• Cláudia Nalon

• Theorem Proving for Temporal Logics of Knowledge or Belief

• Carmen Gago

• Efficient Control of Temporal Reasoning

• Alexander Bolotov

• Automata on Infinite Words and Temporal Logic Normal Forms

• Ullrich Hustadt

• Practical Proof Methods for Combined Modal and Temporal Logics

• Regimantas Pliuškevičius

• A Deductive Decision Procedure for a Restricted FTL

• Markus Moschner

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

11.00 1B27 Poster presentations for Session I and coffee break
12.00 1B06 Invited talk: Maarten de Rijke (University of Amsterdam)

Modal Experiments

13.00  Lunch break
Afternoon Chair: Alan Bundy

14.30 1B06 Session II: Decidable Fragments, Description Logics, Constraints, Proof Planning

• Lilia Georgieva, Ullrich Hustadt, and Renate Schmidt

• Hyperresolution for Guarded Formulae

• Renate Schmidt

• Deciding Fluted Logic with Resolution

• Ulrich Endriss

• Reasoning in Description Logics with Wellington 1.0

• François Beuvron, Martina Kullmann, David Rudloff, Michael Schlick,

• and François Rousselot

• The Description Logic Reasoner CICLOP (Version 2.0)

• Stefan Schlobach

• Description Logics and Knowledge Discovery of Data

• Alan Frisch and Toby Walsh

• Automatic Generation of Implied Constraints

• Richard Boulton

• Towards Automating Inductive Proofs for State Monads

• Mauricio Osorio, Juan Carlos Nieves, and Gabriel Cervantes

• Application of Simplification Theories

15.30 1B27 Poster presentations for Session II and coffee break
16.30 1B06 Invited talk: Rolf Backofen (Ludwig-Maximilians-Universität München)

Exclusion of Symmetries in Search - A Spin-off from Bioinformatics Research

18.00  Leaving King’s for the Wheel; capsules are booked for 18.30
20.00  Buffet at Restaurant Cubana

Automated Reasoning Workshop 2000

Friday, 21 July 2000

Morning  Chair: Alan Frisch
9.00 1B06 Invited talk: Michael Kohlhase (Universität des Saarlandes)

Using Deduction Techniques for Natural Language Understanding

10.00 1B06 Session III: Term Algebras, Theorem Proving, Concurrency • Tatiana Rybina and Andrei Voronkov

• A Decision Procedure for Term Algebras with Queues

• Konstantin Korovin and Andrei Voronkov

• The Existential Theories of Term Algebras with the Knuth-Bendix Orderings • are Decidable

• Alexandre Riazanov and Andrei Voronkov

• System Description: Vampire 1.0

• James Harland, David Pym, and Michael Winikoff

• Forward and Backward Chaining in Linear Logic

• Allan Ramsay

• Run-time Optimisations for Reasoning with Intensional Logics

• Joe Hurd

• Congruence Classes with Logic Variables

• Raul Lopes

• Automatic Generation of Concurrent Provers

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

11.00 1B27 Poster presentations for Session III and coffee break
12.00 1B06 Invited talk: Dov Gabbay (King’s College London)

Goal Directed Mechanisms: Proofs, Interpolation and Abduction Procedures

13.00  Lunch break
Afternoon Chair: Andrei Voronkov

14.30 1B06 Panel: Advances in Temporal and Description Logics Moderator: Ullrich Hustadt Participants: Alexander Bolotov, Ulrich Endriss, Martina Kullmann, Regimantas Pliuškevičius, and Stefan Schlobach

16.00 1B27 Coffee break
16.30 1B06 Closing session