Seventh Workshop on Automated Reasoning


Thursday, 20 July 2000    Friday, 21 July 2000
Morning Chair: Hans Jürgen Ohlbach Morning Chair: Alan Frisch
9.00 1B27 Registration desk open 9.00 1B06 Invited talk: Michael Kohlhase (Saarland University)
Using Deduction Techniques for Natural Language Understanding
10.00 1B06 Session I: Temporal Reasoning, Model Building
  • Anatoli Degiarev 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 Pliuskevicius

  • A Deductive Decision Procedure for a Restricted FTL
  • Markus Moschner

  • Finite Model Building for Propositional Gödel-Logics as an Example for Projective Logics
    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 I
    and coffee break
    11.00 1B27 Poster presentations for Session III
    and coffee break
    12.00 1B06 Invited talk: Maarten the Rijke (University of Amsterdam)
    Modal Experiments
    12.00 1B06 Invited talk: Dov Gabbay (King's College London)
    Goal Directed Mechanisms: Proofs, Interpolation and Abduction Procedures
    13.00   Lunch break 13.00   Lunch break
    Afternoon Chair: Alan Bundy Afternoon Chair: Andrei Voronkov
    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
    14.30 1B06 Panel: Advances in Temporal and Description Logics
    Moderator: Ullrich Hustadt
    Participants: Alexander Bolotov, Ulrich Endriss, Martina Kullmann, Regimantas Pliuskevicius, and Stefan Schlobach
    15.30 1B27 Poster presentations for Session II
    and coffee break
    16.00 1B27 Coffee break
    16.30 1B06 Invited talk: Rolf Backofen (LMU Munich)
    Exclusion of Symmetries in Search - A Spin-off from Bioinformatics Research
    16.30 1B06 Closing session
    18.30   The Wheel (leaving King's at 18.00), buffet at the Cubana, etc.