Timetable
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
Propositional Temporal Resolution Revised Theorem Proving for Temporal Logics of Knowledge or Belief Efficient Control of Temporal Reasoning Automata on Infinite Words and Temporal Logic Normal Forms Practical Proof Methods for Combined Modal and Temporal Logics A Deductive Decision Procedure for a Restricted FTL Finite Model Building for Propositional Gödel-Logics as an Example for Projective Logics |
10.00 | 1B06 | Session III: Term Algebras, Theorem Proving, Concurrency
A Decision Procedure for Term Algebras with Queues The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable System Description: Vampire 1.0 Forward and Backward Chaining in Linear Logic Run-time Optimisations for Reasoning with Intensional Logics Congruence Classes with Logic Variables Automatic Generation of Concurrent Provers 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
Hyperresolution for Guarded Formulae Deciding Fluted Logic with Resolution Reasoning in Description Logics with Wellington 1.0 The Description Logic Reasoner CICLOP (Version 2.0) Description Logics and Knowledge Discovery of Data Automatic Generation of Implied Constraints Towards Automating Inductive Proofs for State Monads 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. |