| 1997 | A Classification of Non-liftable Orders for Resolution. Hans de Nivelle |
| 1997 | A Colored Version of the Lambda-Calculus. Dieter Hutter, Michael Kohlhase |
| 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 |
| 1997 | A New Method for Testing Decision Procedures in Modal Logics. Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani |
| 1997 | A Practical Implementation of Simple Consequence Relations Using Inductive Definitions. Seán Matthews |
| 1997 | A Practical Integration of First-Order Reasoning and Decision Procedures. Nikolaj S. Bjørner, Mark E. Stickel, Tomás E. Uribe |
| 1997 | A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry. Lu Yang, Hongguang Fu, Zhenbing Zeng |
| 1997 | Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. Moshe Y. Vardi |
| 1997 | Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings William McCune |
| 1997 | Automatic Verification of Cryptographic Protocols with SETHEO. Johann Schumann |
| 1997 | CODE: A Powerful Prover for Problems of Condensed Detachment. Dirk Fuchs, Matthias Fuchs |
| 1997 | Connection-Based Proof Construction in Linear Logic. Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt |
| 1997 | Constructing a Normal Form for Property Theory. Mary Cryan, Allan Ramsay |
| 1997 | Decidable Call by Need Computations in term Rewriting (Extended Abstract). Irène Durand, Aart Middeldorp |
| 1997 | Deciding Intuitionistic Propositional Logic via Translation into Classical Logic. Daniel S. Korn, Christoph Kreitz |
| 1997 | Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo |
| 1997 | DiaLog: A System for Dialogue Logic. Jürgen Ehrensberger, Claus Zinn |
| 1997 | Evolving Combinators. Matthias Fuchs |
| 1997 | Exact Kanowledge Compilation in Predicate Calculus: The Partial Achievement Case. Olivier Roussel, Philippe Mathieu |
| 1997 | Hybrid Interactive Theorem Proving Using Nuprl and HOL. Amy P. Felty, Douglas J. Howe |
| 1997 | ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output. Andreas Wolf, Johann Schumann |
| 1997 | Integration of Automated and Interactive Theorem Proving in ILP. Bernd I. Dahn, Jürgen Gehne, Th. Honigmann, Andreas Wolf |
| 1997 | Jape: A Calculator for Animating Proof-on-Paper. Richard Bornat, Bernard Sufrin |
| 1997 | Lemma Matching for a PTTP-based Top-down Theorem Prover. Koji Iwanuma |
| 1997 | Minlog: A Minimal Logic Theorem Prover. John K. Slaney |
| 1997 | Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving. Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura |
| 1997 | Nuprl-Light: An Implementation Framework for Higher-Order Logics. Jason J. Hickey |
| 1997 | Omega: Towards a Mathematical Assistant. Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, Volker Sorge |
| 1997 | On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting. Joachim Niehren, Manfred Pinkal, Peter Ruhrberg |
| 1997 | Partial Matching for Analogy Discovery in Proofs and Counter-Examples. Gilles Défourneaux, Nicolas Peltier |
| 1997 | Plagiator - A Learning Prover. Thomas Kolbe, Jürgen Brauburger |
| 1997 | Proof Tactics for a Theory of State Machines in a Graphical Environment. Katherine A. Eastaughffe, Maris A. Ozols, Anthony Cant |
| 1997 | Proving System Correctness with KIV 3.0. Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel |
| 1997 | RALL: Machine-Supported Proofs for Relation Algebra. David von Oheimb, Thomas F. Gritzner |
| 1997 | Resource-Distribution via Boolean Constraint (Extended Abstract). James Harland, David J. Pym |
| 1997 | SATO: An Efficient Propositional Prover. Hantao Zhang |
| 1997 | SETHEO Goes Software Engineering: Application of ATP to Software Reuse. Bernd Fischer, Johann Schumann |
| 1997 | Soft Typing for Ordered Resolution. Harald Ganzinger, Christoph Meyer, Christoph Weidenbach |
| 1997 | Some Pitfalls of LK-to-LJ Translations and How to Avoid Them. Uwe Egly |
| 1997 | The Char-Set Method and Its Applications to Automated Reasoning. Wu Wen-Tsün |
| 1997 | The Clause-Diffusion Theorem Prover Peers-mcd (System Description). Maria Paola Bonacina |
| 1997 | The Tableau Browser SNARKS. Mathias Kettner, Norbert Eisinger |
| 1997 | Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs. Louise A. Dennis, Alan Bundy, Ian Green |
| 1997 | XBarnacle: Making Theorem Provers More Accessible. Helen Lowe, David Duncan |
| 1997 | XIsabelle: A System Description. Maris A. Ozols, Anthony Cant, Katherine A. Eastaughffe |