| 1997 | The Tableau Browser SNARKS. | Mathias Kettner, Norbert Eisinger |
| 1997 | Lemma Matching for a PTTP-based Top-down Theorem Prover. | Koji Iwanuma |
| 1997 | A Colored Version of the Lambda-Calculus. | Dieter Hutter, Michael Kohlhase |
| 1997 | Nuprl-Light: An Implementation Framework for Higher-Order Logics. | Jason J. Hickey |
| 1997 | Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving. | Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura |
| 1997 | Resource-Distribution via Boolean Constraint (Extended Abstract). | James Harland, David J. Pym |
| 1997 | A New Method for Testing Decision Procedures in Modal Logics. | Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani |
| 1997 | Soft Typing for Ordered Resolution. | Harald Ganzinger, Christoph Meyer, Christoph Weidenbach |
| 1997 | CODE: A Powerful Prover for Problems of Condensed Detachment. | Dirk Fuchs, Matthias Fuchs |
| 1997 | Evolving Combinators. | Matthias Fuchs |
| 1997 | SETHEO Goes Software Engineering: Application of ATP to Software Reuse. | Bernd Fischer, Johann Schumann |
| 1997 | Hybrid Interactive Theorem Proving Using Nuprl and HOL. | Amy P. Felty, Douglas J. Howe |
| 1997 | DiaLog: A System for Dialogue Logic. | Jrgen Ehrensberger, Claus Zinn |
| 1997 | Some Pitfalls of LK-to-LJ Translations and How to Avoid Them. | Uwe Egly |
| 1997 | Proof Tactics for a Theory of State Machines in a Graphical Environment. | Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant |
| 1997 | Decidable Call by Need Computations in term Rewriting (Extended Abstract). | Irne Durand, Aart Middeldorp |
| 1997 | Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs. | Louise A. Dennis, Alan Bundy, Ian Green |
| 1997 | Partial Matching for Analogy Discovery in Proofs and Counter-Examples. | Gilles Dfourneaux, Nicolas Peltier |
| 1997 | Integration of Automated and Interactive Theorem Proving in ILP. | Bernd I. Dahn, Jrgen Gehne, Th. Honigmann, Andreas Wolf |
| 1997 | Constructing a Normal Form for Property Theory. | Mary Cryan, Allan Ramsay |
| 1997 | Jape: A Calculator for Animating Proof-on-Paper. | Richard Bornat, Bernard Sufrin |
| 1997 | The Clause-Diffusion Theorem Prover Peers-mcd (System Description). | Maria Paola Bonacina |
| 1997 | A Practical Integration of First-Order Reasoning and Decision Procedures. | Nikolaj S. Bjrner, Mark E. Stickel, Toms E. Uribe |
| 1997 | Omega: Towards a Mathematical Assistant. | Christoph Benzmller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jrg H. Siekmann, Volker Sorge |
| 1997 | A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. | Franz Baader, Cesare Tinelli |