| 1992 | Programming with Equations: A Framework for Lazy Parallel Evaluation. | R. C. Sekar, I. V. Ramakrishnan |
| 1992 | KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract). | Johann Schumann |
| 1992 | The FAUST - Prover. | Klaus Schneider, Ramayya Kumar, Thomas Kropf |
| 1992 | The KIV System: Systematic Construction of Verified Software. | Wolfgang Reif |
| 1992 | Computing Transivity Tables: A Challenge For Automated Theorem Provers. | David A. Randell, Anthony G. Cohn, Zhan Cui |
| 1992 | Disproving Conjectures. | Martin Protzen |
| 1992 | Implementing the Meta-Theory of Deductive Systems. | Frank Pfenning, Ekkehard Rohwedder |
| 1992 | PVS: A Prototype Verification System. | Sam Owre, John M. Rushby, Natarajan Shankar |
| 1992 | Reduction and Unification in Lambda Calculi with Subtypes. | Tobias Nipkow, Zhenyu Qian |
| 1992 | Isabelle-91. | Tobias Nipkow, Lawrence C. Paulson |
| 1992 | Theorem Proving with Ordering Constrained Clauses. | Robert Nieuwenhuis, Albert Rubio |
| 1992 | Experiments in Automated Deduction with Condensed Detachment. | William McCune, Larry Wos |
| 1992 | Grammar Rewriting. | David A. McAllester |
| 1992 | The Special-Relation Rules are Incomplete. | Zohar Manna, Richard J. Waldinger |
| 1992 | Automatic Program Optimization Through Proof Transformation. | Peter Madden |
| 1992 | Benchmark Problems in Which Equality Plays the Major Role. | Ewing L. Lusk, Larry Wos |
| 1992 | ROO: A Parallel Theorem Prover. | Ewing L. Lusk, William McCune, John K. Slaney |
| 1992 | Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors. | Delia Kesner |
| 1992 | Computing Prime Implicates Incrementally. | Peter Jackson |
| 1992 | Embedding Negation as Failure into a Model Generation Theorem Prover. | Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa |
| 1992 | FRI: Failure-Resistant Induction in RRL. | Xin Hua, Hantao Zhang |
| 1992 | The Central Variable Strategy of Str+ve. | Larry M. Hines |
| 1992 | Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs. | Jane Hesketh, Alan Bundy, Alan Smaill |
| 1992 | MGTP: A Parallel Theorem Prover Based on Lazy Model Generation. | Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita |
| 1992 | An Abstract View of Sorted Unification. | Alan M. Frisch, Anthony G. Cohn |