| 1996 | System Description: Generating Models by SEM. | Jian Zhang, Hantao Zhang |
| 1996 | SPASS & FLOTTER Version 0.42. | Christoph Weidenbach, Bernd Gaede, Georg Rock |
| 1996 | Unification in Pseudo-Linear Sort Theories is Decidable. | Christoph Weidenbach |
| 1996 | GEOTHER: A Geometry Theorem Prover. | Dongming Wang |
| 1996 | Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. | Andrei Voronkov |
| 1996 | An Improved Lower Bound for the Elementary Theories of Trees. | Sergei G. Vorobyov |
| 1996 | Ground Resolution with Group Computations on Semantic Symmetries. | Thierry Boy de la Tour |
| 1996 | A Resolution Theorem Prover for Intuitonistic Logic. | Tanel Tammet |
| 1996 | The Design of the CADE-13 ATP System Competition. | Christian B. Suttner, Geoff Sutcliffe |
| 1996 | Rewrite Semantics for Production Rule Systems: Theory and Applications. | Wayne Snyder, James G. Schmolze |
| 1996 | Termination of Algorithms over Non-freely Generated Data Types. | Claus Sengler |
| 1996 | What Can We Hope to Achieve From Automated Deduction? (Abstract). | Dana S. Scott |
| 1996 | Efficient Model Generation through Compilation. | Heribert Schtz, Tim Geisler |
| 1996 | SiCoTHEO: Simple Competitive Parallel Theorem Provers. | Johann Schumann |
| 1996 | Converting Non-Classical Matrix Proofs into Sequent-Style Systems. | Stephan Schmitt, Christoph Kreitz |
| 1996 | XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description. | Torsten Schaub, Stefan Brning, Pascal Nicolas |
| 1996 | Optimal Axiomatizations for Multiple-Valued Operators and Quantifiers Based on Semi-lattices. | Gernot Salzer |
| 1996 | An Abstract Machine for Fixed-Order Dynamically Stratified Programs. | Konstantinos Sagonas, Terrance Swift, David Scott Warren |
| 1996 | Reflection of Formal Tactics in a Deductive Reflection Framework. | Harald Rue |
| 1996 | A New Method for Knowledge Compilation: The Achievement by Cycle Search. | Olivier Roussel, Philippe Mathieu |
| 1996 | Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract). | Eike Ritter, David J. Pym, Lincoln A. Wallen |
| 1996 | An Embedding of Ruby in Isabelle. | Ole Rasmussen |
| 1996 | Patching Faulty Conjectures. | Martin Protzen |
| 1996 | Partitioning Methods for Satisfiability Testing on Large Formulas. | Tai Joon Park, Allen Van Gelder |
| 1996 | SCAN - Elimination of Predicate Quantifiers. | Hans Jrgen Ohlbach |