FTP97
List of accepted papers

The program committee of FTP97 received 44 submissions, of which 25 were accepted.

• Serge Autexier and Dieter Hutter:
  Equational Proof-Planning by Dynamic Abstraction

• Matthias Baaz and Alexander Leitsch:
  Cut Elimination by Resolution

• Peter Baumgartner and Ulrich Furbach:
  Refinements for Restart Model Elimination

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

• Maria Paola Bonacina:
  On the representation of parallel search in theorem proving

• Thierry Boy de la Tour:
  Up-to-Isomorphism Enumeration of Finite Models - The Monadic Case

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

• Ricardo Caferra and Nicolas Peltier:
  Model building in the cross-roads of consequence and non-consequence relations

• Domenico Cantone, Alessandra Cavarra, and Eugenio Omodeo:
  On existential quantified conjunctions of atomic formulae of L+

• Olga Caprotti:
  Symbolic Pattern Solving for Equational Reasoning

• Ingo Dahn and Christoph Wernhard:
  First Order Proof Problems Extracted from an Article in the MIZAR Mathematical Library

• Marc Fuchs:
  Similarity-Based Lemma Generation for Model Elimination

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

• Alfons Geser and Wolfgang Küchlin:
  Structured Formal Verification of a Fragment of the IBM 390 Clock Chip

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

• John Harrison:
  First Order Logic in Practice

• Robert Matzinger:
  Using Grammars for Finite Domain Evaluation

• Georg Moser:
  Some Remarks on Transfinite E-Semantic Trees and Superposition

• Pierre Ostier:
  A Complete Deduction System for Reasoning with Temporary Assumptions

• Uwe Petermann:
  Building-In Hybrid Theories

• Reinhard Pichler:
  Testing the Equivalence of Models given through Linear Atomic Representations

• Wolfgang Reif and Gerhard Schellhorn:
  Theorem Proving in Large Theories

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

• Uwe Waldmann:
  A Superposition Calculus for Divisible Torsion-Free Abelian Groups

• Nic Wilson and Jerome Mengin:
  Logical Deduction using the Local Computation Framework