@inproceedings{autexier97FTP,
	crossref="FTP97",
	title="Equational Proof-Planning by Dynamic Abstraction",
	author="Serge Autexier and Dieter Hutter",
	pages="1--6"
}
	
@inproceedings{baaz97FTP,
	crossref="FTP97",
	title="Cut Elimination by Resolution",
	author="Matthias Baaz and Alexander Leitsch",
	pages="7--10"
}

@inproceedings{baumgart97FTP,
	crossref="FTP97",
	title="Refinements for Restart Model Elimination",
	author="Peter Baumgartner and Ulrich Furbach",
	pages="11--16"
}

@inproceedings{bierwald97FTP,
	crossref="FTP97",
	title="Tableau Prover Tatzelwurm: Hyper-Links and UR-Resolution",
	author="Carsten Bierwald and Thomas K{\"a}ufl",
	pages="17--21"
}

@inproceedings{bonacina97FTP,
	crossref="FTP97",
	title="On the representation of parallel search in theorem proving",
	author="Maria Paola Bonacina",
	pages="22--28"
}

@inproceedings{boydelat97FTP,
	crossref="FTP97",
	title="Up-to-Isomorphism Enumeration of Finite 
               Models---The Monadic Case",
	author="Boy de la Tour, Thierry",
	pages="29--33"
}

@inproceedings{brandl97FTP,
	crossref="FTP97",
	title="Testing for Renamability to Classes of Clause Sets",
	author="Albert Brandl and Christian G. Ferm{\"u}ller and Gernot Salzer",
	pages="34--39"
}

@inproceedings{caferra97FTP,
	crossref="FTP97",
	title="Model building in the cross-roads of consequence and 
               non-consequence relations",
	author="Ricardo Caferra and Nicolas Peltier",
	pages="40--44"
}

@inproceedings{cantone97FTP,
	crossref="FTP97",
	title="On existential quantified conjunctions of atomic formulae of
               {${\cal L}^+$}",
	author="Domenico Cantone and Alessandra Cavarra and Eugenio Omodeo",
	pages="45--52"
}

@inproceedings{caprotti97FTP,
	crossref="FTP97",
	title="Symbolic Pattern Solving for Equational Reasoning",
	author="Olga Caprotti",
	pages="53--57"
}

@inproceedings{dahn97FTP,
	crossref="FTP97",
	title="First Order Proof Problems Extracted from an Article 
               in the MIZAR Mathematical Library",
	author="Ingo Dahn and Christoph Wernhard",
	pages="58--62"
}

@inproceedings{fuchs97FTP,
	crossref="FTP97",
	title="Similarity-Based Lemma Generation for Model Elimination",
	author="Marc Fuchs",
	pages="63--67"
}

@inproceedings{gascard97FTP,
	crossref="FTP97",
	title="Two Approaches to the Formal Proof of Replicated 
               Hardware Systems using the Boyer-Moore Theorem Prover",
	author="Eric Gascard and Laurence Pierre",
	pages="68--72"
}

@inproceedings{geser97FTP,
	crossref="FTP97",
	title="Structured Formal Verification of a Fragment of the 
               IBM 390 Clock Chip",
	author="Alfons Geser and Wolfgang K{\"u}chlin",
	pages="73--77"
}

@inproceedings{goguen97FTP,
	crossref="FTP97",
	title="Stretching First Order Equational Logic: Proofs with 
               Partiality, Subtypes and Retracts",
	author="Joseph A. Goguen",
	pages="78--85"
}

@inproceedings{harrison97FTP,
	crossref="FTP97",
	title="First Order Logic in Practice",
	author="John Harrison",
	pages="86--90"
}
@inproceedings{matzinge97FTP,
	crossref="FTP97",
	title="Using Grammars for Finite Domain Evaluation",
	author="Robert Matzinger",
	pages="91--96"
}

@inproceedings{moser97FTP,
	crossref="FTP97",
	title="Some Remarks on Transfinite E-Semantic Trees and 
               Superposition",
	author="Georg Moser",
	pages="97--102"
}

@inproceedings{ostier97FTP,
	crossref="FTP97",
	title="A Complete Deduction System for Reasoning with 
               Temporary Assumptions",
	author="Pierre Ostier",
	pages="103--107"
}

@inproceedings{peterman97FTP,
	crossref="FTP97",
	title="Building-In Hybrid Theories",
	author="Uwe Petermann",
	pages="108--112"
}

@inproceedings{pichler97FTP,
	crossref="FTP97",
	title="Testing the Equivalence of Models given through 
               Linear Atomic Representations",
	author="Reinhard Pichler",
	pages="113--118"
}

@inproceedings{reif97FTP,
	crossref="FTP97",
	title="Theorem Proving in Large Theories",
	author="Wolfgang Reif and Gerhard Schellhorn",
	pages="119--124"
}

@inproceedings{stuber97FTP,
	crossref="FTP97",
	title="Strong Symmetrization and Semi-Compatibility of 
               Normalized Rewriting and First-Order Theorem Proving",
	author="J{\"u}rgen Stuber",
	pages="125--129"
}

@inproceedings{waldmann97FTP,
	crossref="FTP97",
	title="A Superposition Calculus for Divisible Torsion-Free 
               Abelian Groups",
	author="Uwe Waldmann",
	pages="130--134"
}

@inproceedings{wilson97FTP,
	crossref="FTP97",
	title="Logical Deduction using the Local Computation Framework",
	author="Nic Wilson and Jerome Mengin",
	pages="135--139"
}

@proceedings{FTP97,
        editor={Maria Paola Bonacina and Ulrich Furbach},
        title={Int. Workshop on First-Order Theorem Proving (FTP'97)},
        booktitle={Int. Workshop on First-Order Theorem Proving (FTP'97)},
        year={1997},
        series={RISC-Linz Report Series No. 97-50},
        publisher={Johannes Kepler Universit\"at, Linz (Austria)}
}