FTP97 International Workshop on First order Theorem Proving Schloss Hagenberg, Austria October 27 - 28, 1997

Appeared in the RISC-Linz Report Series, No. 97-50, Johannes Kepler Universität Linz (Austria), 1997.

The proceedings can be downloaded one paper at a time by following the links below, or as a single gzipped tar-archive (2.6 MB) which expands to 7.6 MB (see the README file for further details). The bibliographic data for all articles is available in BibTeX format.

Cover page

Preface

Invited talk

• The Theorema Project: An Overview
  Bruno Buchberger

Contributed papers

All submissions were refereed by two or three referees. The program committee accepted 25 out of 44 papers.

• Equational Proof-Planning by Dynamic Abstraction
  Serge Autexier and Dieter Hutter, pages 1-6

• Cut Elimination by Resolution
  Matthias Baaz and Alexander Leitsch, pages 7-10

• Refinements for Restart Model Elimination
  Peter Baumgartner and Ulrich Furbach, pages 11-16

• Tableau Prover Tatzelwurm: Hyper-Links and UR-Resolution
  Carsten Bierwald and Thomas Käufl, pages 17-21

• On the representation of parallel search in theorem proving
  Maria Paola Bonacina, pages 22-28

• Up-to-Isomorphism Enumeration of Finite Models -- The Monadic Case
  Thierry Boy de la Tour, pages 29-33

• Testing for Renamability to Classes of Clause Sets
  Albert Brandl, Christian G. Fermüller, and Gernot Salzer, pages 34-39

• Model building in the cross-roads of consequence and non-consequence relations
  Ricardo Caferra and Nicolas Peltier, pages 40-44

• On existential quantified conjunctions of atomic formulae of L+
  Domenico Cantone, Alessandra Cavarra, and Eugenio Omodeo, pages 45-52

• Symbolic Pattern Solving for Equational Reasoning
  Olga Caprotti, pages 53-57

• First Order Proof Problems Extracted from an Article in the MIZAR Mathematical Library
  Ingo Dahn and Christoph Wernhard, pages 58-62

• Similarity-Based Lemma Generation for Model Elimination
  Marc Fuchs, pages 63-67

• Two Approaches to the Formal Proof of Replicated Hardware Systems using the Boyer-Moore Theorem Prover
  Eric Gascard and Laurence Pierre, pages 68-72

• Structured Formal Verification of a Fragment of the IBM 390 Clock Chip
  Alfons Geser and Wolfgang Küchlin, pages 73-77

• Stretching First Order Equational Logic: Proofs with Partiality, Subtypes and Retracts
  Joseph A. Goguen, pages 78-85

• First Order Logic in Practice
  John Harrison, pages 86-90

• Using Grammars for Finite Domain Evaluation
  Robert Matzinger, pages 91-96

• Some Remarks on Transfinite E-Semantic Trees and Superposition
  Georg Moser, pages 97-102

• A Complete Deduction System for Reasoning with Temporary Assumptions
  Pierre Ostier, pages 103-107

• Building-In Hybrid Theories
  Uwe Petermann, pages 108-112

• Testing the Equivalence of Models given through Linear Atomic Representations
  Reinhard Pichler, pages 113-118

• Theorem Proving in Large Theories
  Wolfgang Reif and Gerhard Schellhorn, pages 119-124

• Strong Symmetrization, Semi-Compatibility of Normalized Rewriting and First-Order Theorem Proving
  Jürgen Stuber, pages 125-129

• A Superposition Calculus for Divisible Torsion-Free Abelian Groups
  Uwe Waldmann, pages 130-134

• Logical Deduction using the Local Computation Framework
  Nic Wilson and Jerome Mengin, pages 135-139