| 1996 | Resolution-Based Calculi for Modal and Temporal Logics. | Andreas Nonnengart |
| 1996 | More Church-Rosser Proofs (in Isabelle/HOL). | Tobias Nipkow |
| 1996 | Transforming Termination by Self-Labelling. | Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema |
| 1996 | Internal Analogy in Theorem Proving. | Erica Melis, Jon Whittle |
| 1996 | Walther Recursion. | David A. McAllester, Kostas Arkoudas |
| 1996 | Theorem Proving with Group Presentations: Examples and Questions. | Ursula Martin |
| 1996 | Grammar Specification in Categorial Logics and Theorem Proving. | Saturnino F. Luz-Filho |
| 1996 | Algebra and Automated Deduction. | Steve Linton, Ursula Martin, Pter Prhle, Duncan Shand |
| 1996 | Termination of Theorem Proving by Reuse. | Thomas Kolbe, Christoph Walther |
| 1996 | Lemma Discovery in Automated Induction. | Deepak Kapur, Mahadevan Subramaniam |
| 1996 | Extensions to a Generalization Critic for Inductive Proof. | Andrew Ireland, Alan Bundy |
| 1996 | INKA: The Next Generation. | Dieter Hutter, Claus Sengler |
| 1996 | Presenting Machine-Found Proofs. | Xiaorong Huang, Armin Fiedler |
| 1996 | Mechanical Verification of Mutually Recursive Procedures. | Peter V. Homeier, David F. Martin |
| 1996 | Unification Algorithms Cannot be Combined in Polynomial Time. | Miki Hermann, Phokion G. Kolaitis |
| 1996 | Optimizing Proof Search in Model Elimination. | John Harrison |
| 1996 | Unification and Matching Modulo Nilpotence. | Qing Guo, Paliath Narendran, David A. Wolfram |
| 1996 | Advanced Indexing Operations on Substitution Trees. | Peter Graf, Christoph Meyer |
| 1996 | Path Indexing for AC-Theories. | Peter Graf |
| 1996 | ABSFOL: A Proof Checker with Abstraction. | Fausto Giunchiglia, Adolfo Villafiorita |
| 1996 | Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. | Fausto Giunchiglia, Roberto Sebastiani |
| 1996 | Tableaux and Algorithms for Propositional Dynamic Logic with Converse. | Giuseppe De Giacomo, Fabio Massacci |
| 1996 | Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). | Harald Ganzinger, Uwe Waldmann |
| 1996 | Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). | Harald Ganzinger |
| 1996 | Experiments in the Heuristic Use of Past Proof Experience. | Matthias Fuchs |