First Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice

Forward . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . i Timetable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Position Papers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

Peter Baumgartner (with Ulrich Furbach) The Spectrum of Model Elimination Based Theorem Proving . . . . . . . . . . . . . . . . . . . 5 Bernhard Beckert (with Joachim Posegga) Lean Theorem Proving: Maximal Efficiency from Minimal Means . . . . . . . . . . . . . . . . . 7 John Bell Pragmatic Reasoning: A model-building manifesto . . . . . . . . . . . . . . . . . . . . . . . . . 9 Antony Cohn Reasoning about space . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Jim Cunningham Reasoning About Large Specifications - How is it Possible? . . . . . . . . . . . . . . . . . . . . 13 Eric de Kogel A Simple Algorithm for Rigid E-Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 John Derrick (with Gyuri Lajos) Theory and Practice in Applying Proof Development Systems to Specification and Verification for Synchronous Concurrent Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Harrie C.M. de Swart Tableaux versus Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Andre de Waal (with John P. Gallagher) (see John P. Gallagher below) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . David A. Duffy A Classical View of Inductionless Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Alan M. Frisch (with C. David Page Jr.) Wanted: A Theory for Approximation for Automated Reasoning . . . . . . . . . . . . . . . . . 24 Ulrich Furbach (with Peter Baumgartner) (see Peter Baumgartner above) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . John P. Gallagher (with Andre de Waal) Exploiting the Speed and Simplicity of Incomplete Proof Procedures . . . . . . . . . . . . . . . 26 Antony Galton Automating Temporal Non-Monotonic Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . 28

John Gooday Nonmonotonic Temporal Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

Anthony Griffiths Case Retrieval for Mixed Paradigm Problem Solvers . . . . . . . . . . . . . . . . . . . . . . . . 30

Reiner Hahnle (with Wolfgang Reif) Towards the Integration of Tactical and Automated Reasoning . . . . . . . . . . . . . . . . . . 32

Pat M. Hill Declarative Meta-Programming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

Andrew Ireland (with Alan Bundy) Proof Plans: Bridging Gaps in Formal Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . 37

Robert Johnson The Practical Implementation of Temporal Theorem-Provers over Novel Parallel Architectures 39

Robert Kowalski Logic Progams for Temporal Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

John Lee Graphics as an Aid to Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

Yuh-jeng Lee Automated Rule Updating in a Deductive Simulation Model: A practical Application of Inductive Learning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

Craig MacNish Towards Practical Nonmonotonic Temporal Reasoning . . . . . . . . . . . . . . . . . . . . . . . 46

C. David Page Jr. (with Alan M. Frisch) (See Alan M. Frisch above) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Rashmi Pandya Numerical approaches to probatility in AI and the concept of Logical Reasoning . . . . . . . . 48

Wolfgang Reif Specifying and Veryfying Large Software Systems with KIV (see also Reiner Haehnle above) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

Anton Setzer A Type Theory with Specific Proof Theoretic Behaviour . . . . . . . . . . . . . . . . . . . . . . 53

Mark Tarver A Typed Functional Language Based on Sequent Calculus . . . . . . . . . . . . . . . . . . . . . 55

List of Participants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57