- Peter Jackson, John Pais:
Computing Prime Implicants. CADE 1990: 543-557 - Thomas Käufl, Nicolas Zabel:
The Theorem Prover of the Program Verifier Tatzelwurm. CADE 1990: 657-658 - Matt Kaufmann:
RCL: A Lisp Verification System. CADE 1990: 659-660 - Claude Kirchner:
Tutorial on Equational Unification. CADE 1990: 682 - Sang Ho Lee, Lawrence J. Henschen:
Substitution-based Compilation of Extended Rules in Deductive Databases. CADE 1990: 57-71 - Pierre Lescanne:
ORME: An Implementation of Completion Procedures as Sets of Transition Rules. CADE 1990: 661-662 - Ewing L. Lusk, William McCune:
Tutorial on High-Performance Automated Theorem Proving. CADE 1990: 681 - Ursula Martin, Tobias Nipkow:
Ordered Rewriting and Confluence. CADE 1990: 366-380 - William McCune:
OTTER 2.0. CADE 1990: 663-664 - Alan F. McMichael:
SLIM: An Automated Reasoner For Equivalences, Applied To Set Theory. CADE 1990: 308-321 - Jürgen Müller, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka:
Tutorial on Reasoning and Representation with Concept Languages. CADE 1990: 681 - Neil V. Murray, Erik Rosenthal:
DISSOLVER: A Dissolution-based Theorem Prover. CADE 1990: 665-666 - Paliath Narendran, Friedrich Otto:
Some Results on Equational Unification. CADE 1990: 276-291 - Xumin Nie, David A. Plaisted:
A Complete Semantic Back Chaining Proof System. CADE 1990: 16-27 - Robert Nieuwenhuis, Fernando Orejas, Albert Rubio:
TRIP: An Implementation of Clausal Rewriting. CADE 1990: 667-668 - Werner Nutt:
Unification in Monoidal Theories. CADE 1990: 618-632 - Hans Jürgen Ohlbach, Andreas Herzig:
Tutorial on Compilation techniques for Logics. CADE 1990: 683 - Yusuf Ozturk, Lawrence J. Henschen:
Hyper Resolution and Equality Axioms without Function Substitutions. CADE 1990: 456-469 - Gerald E. Peterson:
Complete Sets of Reductions with Constraints. CADE 1990: 381-395 - Frank Pfenning, Dan Nesmith:
Presenting Intuitive Deductions via Symmetric Simplification. CADE 1990: 336-350 - William Pierce:
Toward Mechanical Methods for Streamlining Proofs. CADE 1990: 351-365 - John L. Pollock:
OSCAR. CADE 1990: 669-670 - Paul Pritchard, John K. Slaney:
Tutorial on Computing Models of Propositional Logics. CADE 1990: 685 - David J. Pym, Lincoln A. Wallen:
Investigations into Proof-Search in a System of First-Order Dependent Function Types. CADE 1990: 236-250 - Uday S. Reddy:
Term Rewriting Induction. CADE 1990: 162-177 - Mikael Rittri:
Retrieving Library Identifiers via Equational Matching of Types. CADE 1990: 603-617 - Ronald W. Satz:
EXPERT THINKER: An Adaptation of F-Prolog to Microcomputers. CADE 1990: 671-672 - Johann Schumann, Reinhold Letz:
PARTHEO: A High-Performance Parallel Theorem Prover. CADE 1990: 40-56 - Johann Schumann, Reinhold Letz, Franz J. Kurfess:
Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation. CADE 1990: 683 - Camilla Schwind:
A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic. CADE 1990: 528-542