| 1996 | A New Method for Knowledge Compilation: The Achievement by Cycle Search. Olivier Roussel, Philippe Mathieu |
| 1996 | A Resolution Theorem Prover for Intuitonistic Logic. Tanel Tammet |
| 1996 | ABSFOL: A Proof Checker with Abstraction. Fausto Giunchiglia, Adolfo Villafiorita |
| 1996 | Advanced Indexing Operations on Substitution Trees. Peter Graf, Christoph Meyer |
| 1996 | Algebra and Automated Deduction. Steve Linton, Ursula Martin, Péter Pröhle, Duncan Shand |
| 1996 | An Abstract Machine for Fixed-Order Dynamically Stratified Programs. Konstantinos Sagonas, Terrance Swift, David Scott Warren |
| 1996 | An Embedding of Ruby in Isabelle. Ole Rasmussen |
| 1996 | An Improved Lower Bound for the Elementary Theories of Trees. Sergei G. Vorobyov |
| 1996 | An Introduction to Geometry Expert. Shang-Ching Chou, Xiao-Shan Gao, Jing-Zhong Zhang |
| 1996 | Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings Michael A. McRobbie, John K. Slaney |
| 1996 | Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. Fausto Giunchiglia, Roberto Sebastiani |
| 1996 | Converting Non-Classical Matrix Proofs into Sequent-Style Systems. Stephan Schmitt, Christoph Kreitz |
| 1996 | CtCoq: A System Presentation. Janet Bertot, Yves Bertot |
| 1996 | Efficient Model Generation through Compilation. Heribert Schütz, Tim Geisler |
| 1996 | Experiments in the Heuristic Use of Past Proof Experience. Matthias Fuchs |
| 1996 | Extensions to a Generalization Critic for Inductive Proof. Andrew Ireland, Alan Bundy |
| 1996 | FasTraC: A Decentralized Traffic Control System Based on Logic Programming. Giovanni Felici, Giovanni Rinaldi, Klaus Truemper |
| 1996 | GEOTHER: A Geometry Theorem Prover. Dongming Wang |
| 1996 | Grammar Specification in Categorial Logics and Theorem Proving. Saturnino F. Luz-Filho |
| 1996 | Ground Resolution with Group Computations on Semantic Symmetries. Thierry Boy de la Tour |
| 1996 | IMPS: An Updated System Description. William M. Farmer, Joshua D. Guttman, F. Javier Thayer |
| 1996 | INKA: The Next Generation. Dieter Hutter, Claus Sengler |
| 1996 | Internal Analogy in Theorem Proving. Erica Melis, Jon Whittle |
| 1996 | Learning Domain Knowledge to Improve Theorem Proving. Jörg Denzinger, Stephan Schulz |
| 1996 | Lemma Discovery in Automated Induction. Deepak Kapur, Mahadevan Subramaniam |
| 1996 | MUltlog 1.0: Towards an Expert System for Many-Valued Logics. Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach |
| 1996 | Mechanical Verification of Mutually Recursive Procedures. Peter V. Homeier, David F. Martin |
| 1996 | More Church-Rosser Proofs (in Isabelle/HOL). Tobias Nipkow |
| 1996 | On Shostak's Decision Procedure for Combinations of Theories. David Cyrluk, Patrick Lincoln, Natarajan Shankar |
| 1996 | On the Practical Value of Different Definitional Translations to Normal Form. Uwe Egly, Thomas Rath |
| 1996 | Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices. Gernot Salzer |
| 1996 | Optimizing Proof Search in Model Elimination. John Harrison |
| 1996 | Partitioning Methods for Satisfiability Testing on Large Formulas. Tai Joon Park, Allen Van Gelder |
| 1996 | Patching Faulty Conjectures. Martin Protzen |
| 1996 | Path Indexing for AC-Theories. Peter Graf |
| 1996 | Presenting Machine-Found Proofs. Xiaorong Huang, Armin Fiedler |
| 1996 | Proof Search with Set Variable Instantiation in the Calculus of Constructions. Amy P. Felty |
| 1996 | Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. Andrei Voronkov |
| 1996 | Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract). Eike Ritter, David J. Pym, Lincoln A. Wallen |
| 1996 | Reflection of Formal Tactics in a Deductive Reflection Framework. Harald Rueß |
| 1996 | Resolution-Based Calculi for Modal and Temporal Logics. Andreas Nonnengart |
| 1996 | Rewrite Semantics for Production Rule Systems: Theory and Applications. Wayne Snyder, James G. Schmolze |
| 1996 | SCAN - Elimination of Predicate Quantifiers. Hans Jürgen Ohlbach |
| 1996 | SPASS & FLOTTER Version 0.42. Christoph Weidenbach, Bernd Gaede, Georg Rock |
| 1996 | Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). Harald Ganzinger |
| 1996 | Search Strategies for Resolution in Temporal Logics. Clare Dixon |
| 1996 | Semantic Trees Revisited: Some New Completeness Results. Christian G. Fermüller |
| 1996 | SiCoTHEO: Simple Competitive Parallel Theorem Provers. Johann Schumann |
| 1996 | Structuring Metatheory on Inductive Definitions. David A. Basin, Seán Matthews |
| 1996 | System Description: Generating Models by SEM. Jian Zhang, Hantao Zhang |
| 1996 | Tableaux and Algorithms for Propositional Dynamic Logic with Converse. Giuseppe De Giacomo, Fabio Massacci |
| 1996 | Termination of Algorithms over Non-freely Generated Data Types. Claus Sengler |
| 1996 | Termination of Theorem Proving by Reuse. Thomas Kolbe, Christoph Walther |
| 1996 | The Design of the CADE-13 ATP System Competition. Christian B. Suttner, Geoff Sutcliffe |
| 1996 | The Tableau-based Theorem Prover Bernhard Beckert, Reiner Hähnle, Peter Oel, Martin Sulzmann |
| 1996 | Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). Harald Ganzinger, Uwe Waldmann |
| 1996 | Theorem Proving with Group Presentations: Examples and Questions. Ursula Martin |
| 1996 | Transforming Termination by Self-Labelling. Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema |
| 1996 | Unification Algorithms Cannot be Combined in Polynomial Time. Miki Hermann, Phokion G. Kolaitis |
| 1996 | Unification and Matching Modulo Nilpotence. Qing Guo, Paliath Narendran, David A. Wolfram |
| 1996 | Unification in Pseudo-Linear Sort Theories is Decidable. Christoph Weidenbach |
| 1996 | Walther Recursion. David A. McAllester, Kostas Arkoudas |
| 1996 | What Can We Hope to Achieve From Automated Deduction? (Abstract). Dana S. Scott |
| 1996 | XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description. Torsten Schaub, Stefan Brüning, Pascal Nicolas |