FTP97International Workshop on

Appeared in the RISCLinz Report Series, No. 9750, 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 tararchive (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.
The Theorema Project: An Overview
Bruno Buchberger
All submissions were refereed by two or three referees. The program committee accepted 25 out of 44 papers.
Equational ProofPlanning by Dynamic Abstraction
Serge Autexier and Dieter Hutter,
pages 16
Cut Elimination by Resolution
Matthias Baaz and Alexander Leitsch,
pages 710
Refinements for Restart Model Elimination
Peter Baumgartner and Ulrich Furbach,
pages 1116
Tableau Prover Tatzelwurm: HyperLinks and URResolution
Carsten Bierwald and Thomas Käufl,
pages 1721
On the representation of parallel search in theorem proving
Maria Paola Bonacina,
pages 2228
UptoIsomorphism Enumeration of Finite Models  The Monadic Case
Thierry Boy de la Tour,
pages 2933
Testing for Renamability to Classes of Clause Sets
Albert Brandl, Christian G. Fermüller, and Gernot Salzer,
pages 3439
Model building in the crossroads of consequence and nonconsequence relations
Ricardo Caferra and Nicolas Peltier,
pages 4044
On existential quantified conjunctions of atomic formulae of L+
Domenico Cantone, Alessandra Cavarra, and Eugenio Omodeo,
pages 4552
Symbolic Pattern Solving for Equational Reasoning
Olga Caprotti,
pages 5357
First Order Proof Problems Extracted from an Article in the MIZAR Mathematical Library
Ingo Dahn and Christoph Wernhard,
pages 5862
SimilarityBased Lemma Generation for Model Elimination
Marc Fuchs,
pages 6367
Two Approaches to the Formal Proof of Replicated Hardware Systems using the BoyerMoore Theorem Prover
Eric Gascard and Laurence Pierre,
pages 6872
Structured Formal Verification of a Fragment of the IBM 390 Clock Chip
Alfons Geser and Wolfgang Küchlin,
pages 7377
Stretching First Order Equational Logic: Proofs with Partiality, Subtypes and Retracts
Joseph A. Goguen,
pages 7885
First Order Logic in Practice
John Harrison,
pages 8690
Using Grammars for Finite Domain Evaluation
Robert Matzinger,
pages 9196
Some Remarks on Transfinite ESemantic Trees and Superposition
Georg Moser,
pages 97102
A Complete Deduction System for Reasoning with Temporary Assumptions
Pierre Ostier,
pages 103107
BuildingIn Hybrid Theories
Uwe Petermann,
pages 108112
Testing the Equivalence of Models given through Linear Atomic Representations
Reinhard Pichler,
pages 113118
Theorem Proving in Large Theories
Wolfgang Reif and Gerhard Schellhorn,
pages 119124
Strong Symmetrization, SemiCompatibility of Normalized Rewriting and FirstOrder Theorem Proving
Jürgen Stuber,
pages 125129
A Superposition Calculus for Divisible TorsionFree Abelian Groups
Uwe Waldmann,
pages 130134
Logical Deduction using the Local Computation Framework
Nic Wilson and Jerome Mengin,
pages 135139