| 1990 | 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings Mark E. Stickel |
| 1990 | A Complete Semantic Back Chaining Proof System. Xumin Nie, David A. Plaisted |
| 1990 | A General Clause Theorem Prover. Geoff Sutcliffe |
| 1990 | A High-Performance Parallel Theorem Prover. Ralph Butler, Ian T. Foster, Anita Jindal, Ross A. Overbeek |
| 1990 | A Mechanically Assisted Constructive Proof in Category Theory. James A. Altucher, Prakash Panangaden |
| 1990 | A Prolog Technology Theorem Prover. Mark E. Stickel |
| 1990 | A Resolution Principle for Clauses with Constraints. Hans-Jürgen Bürckert |
| 1990 | A Science of Reasoning: Extended Abstract. Alan Bundy |
| 1990 | A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic. Camilla Schwind |
| 1990 | A Theorem Prover for a Computational Logic. Robert S. Boyer, J Strother Moore |
| 1990 | ACE: The Abstract Clause Engine. David A. Wolfram |
| 1990 | An Examination of the Prolog Technology Theorem-Prover. Mark Tarver |
| 1990 | An Improved General E-Unification Method. Daniel J. Dougherty, Patricia Johann |
| 1990 | Automated Reasoning Contributed to Mathematics and Logic. Larry Wos, Steve Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler |
| 1990 | Automatic Acquisition of Search Guiding Heuristics. Christian B. Suttner, Wolfgang Ertel |
| 1990 | Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation. Newton C. A. da Costa, Lawrence J. Henschen, James J. Lu, V. S. Subrahmanian |
| 1990 | Case-Free Programs: An Abstraction of Definite Horn Programs. Toshiro Wakayama, T. H. Payne |
| 1990 | Complete Sets of Reductions with Constraints. Gerald E. Peterson |
| 1990 | Computing Prime Implicants. Peter Jackson, John Pais |
| 1990 | Cylindric Algebra Equation Solver. Frank M. Brown, Carlos Araya |
| 1990 | DISSOLVER: A Dissolution-based Theorem Prover. Neil V. Murray, Erik Rosenthal |
| 1990 | Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic. Heikki Tuominen |
| 1990 | EXPERT THINKER: An Adaptation of F-Prolog to Microcomputers. Ronald W. Satz |
| 1990 | Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language. Amy P. Felty, Dale Miller |
| 1990 | Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete. David A. Basin |
| 1990 | Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs. Alan Bundy, Frank van Harmelen, Alan Smaill, Andrew Ireland |
| 1990 | Generalized Well-founded Semantics for Logic Programs (Extended Abstract). Chitta Baral, Jorge Lobo, Jack Minker |
| 1990 | Guiding Induction Proofs. Dieter Hutter |
| 1990 | Higher Order E-Unification. Wayne Snyder |
| 1990 | Hyper Resolution and Equality Axioms without Function Substitutions. Yusuf Ozturk, Lawrence J. Henschen |
| 1990 | IMPS: An Interactive Mathematical Proof System. William M. Farmer, Joshua D. Guttman, F. Javier Thayer |
| 1990 | Improving Assoviative Path Orderings. Joachim Steinbach |
| 1990 | Investigations into Proof-Search in a System of First-Order Dependent Function Types. David J. Pym, Lincoln A. Wallen |
| 1990 | LISS - The Logic Inference Search System. Andrei Voronkov |
| 1990 | Minimizing the Number of Clauses by Renaming. Thierry Boy de la Tour |
| 1990 | ORME: An Implementation of Completion Procedures as Sets of Transition Rules. Pierre Lescanne |
| 1990 | OSCAR. John L. Pollock |
| 1990 | OTTER 2.0. William McCune |
| 1990 | On Restrictions of Ordered Paramodulation with Simplification. Leo Bachmair, Harald Ganzinger |
| 1990 | Ordered Rewriting and Confluence. Ursula Martin, Tobias Nipkow |
| 1990 | PARTHEO: A High-Performance Parallel Theorem Prover. Johann Schumann, Reinhold Letz |
| 1990 | Parallelizing the Closure Computation in Automated Deduction. John K. Slaney, Ewing L. Lusk |
| 1990 | Perspectives on Automated Deduction (Abstract). Wolfgang Bibel |
| 1990 | Presenting Intuitive Deductions via Symmetric Simplification. Frank Pfenning, Dan Nesmith |
| 1990 | Programming by Example and Proving by Example Using Higher-order Unification. Masami Hagiya |
| 1990 | RCL: A Lisp Verification System. Matt Kaufmann |
| 1990 | Retrieving Library Identifiers via Equational Matching of Types. Mikael Rittri |
| 1990 | Rewrite Systems for Varieties of Semigroups. Franz Baader |
| 1990 | Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving. Shang-Ching Chou, Xiao-Shan Gao |
| 1990 | SLIM: An Automated Reasoner For Equivalences, Applied To Set Theory. Alan F. McMichael |
| 1990 | Schemata. Frank M. Brown, Carlos Araya |
| 1990 | Simultaneous Paramodulation. Dan Benanav |
| 1990 | Some Results on Equational Unification. Paliath Narendran, Friedrich Otto |
| 1990 | Str+ve-Subset: The Str+ve-based Subset Prover. Larry M. Hines |
| 1990 | Substitution-based Compilation of Extended Rules in Deductive Databases. Sang Ho Lee, Lawrence J. Henschen |
| 1990 | TRIP: An Implementation of Clausal Rewriting. Robert Nieuwenhuis, Fernando Orejas, Albert Rubio |
| 1990 | Tactical Theorem Proving in Program Verification. Maritta Heisel, Wolfgang Reif, Werner Stephan |
| 1990 | Term Rewriting Induction. Uday S. Reddy |
| 1990 | The Oyster-Clam System. Alan Bundy, Frank van Harmelen, Christian Horn, Alan Smaill |
| 1990 | The Romulus Proof Checker. Carl Eichenlaub, Bruce Esrig, James Hook, Carl Klapper, Garrel Pottinger |
| 1990 | The TPS Theorem Proving System. Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning |
| 1990 | The Theorem Prover of the Program Verifier Tatzelwurm. Thomas Käufl, Nicolas Zabel |
| 1990 | Toward Mechanical Methods for Streamlining Proofs. William Pierce |
| 1990 | Tutorial on Compilation techniques for Logics. Hans Jürgen Ohlbach, Andreas Herzig |
| 1990 | Tutorial on Computing Models of Propositional Logics. Paul Pritchard, John K. Slaney |
| 1990 | Tutorial on Equational Unification. Claude Kirchner |
| 1990 | Tutorial on High-Performance Automated Theorem Proving. Ewing L. Lusk, William McCune |
| 1990 | Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation. Johann Schumann, Reinhold Letz, Franz J. Kurfess |
| 1990 | Tutorial on Lambda-Prolog. Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning |
| 1990 | Tutorial on Program-Synthetic Deduction. Richard J. Waldinger |
| 1990 | Tutorial on Reasoning and Representation with Concept Languages. Jürgen Müller, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka |
| 1990 | Tutorial on Rewrite-Based Theorem Proving. Jieh Hsiang, Jean-Pierre Jouannaud |
| 1990 | UNICOM: A Refined Completion Based Inductive Theorem Prover. Bernhard Gramlich |
| 1990 | Unification in Monoidal Theories. Werner Nutt |
| 1990 | Unification in a Combination of Equational Theories: an Efficient Algorithm. Alexandre Boudet |