• 
  Ewing L. Lusk, Ross A. Overbeek (Eds.): 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings. Springer 1988 Lecture Notes in Computer Science ISBN 3-540-19343-X

Session 1

• 
  Hantao Zhang, Deepak Kapur: First-Order Theorem Proving Using Conditional Rewrite Rules. 1-20
• 
  Tie-Cheng Wang: Elements of Z-Module Reasoning. 21-40

Session 2

• 
  Michael R. Donat, Lincoln A. Wallen: Learning and Applying Generalised Solutions using Higher Order Resolution. 41-60
• 
  Amy P. Felty, Dale Miller: Specifying Theorem Provers in a Higher-Order Logic Programming Language. 61-80
• 
  V. S. Subrahmanian: Query Processing in Quantitative Logic Programming. 81-100

Session 3

• 
  David A. Basin: An Environment For Automated Reasoning About Partial Functions. 101-110
• 
  Alan Bundy: The Use of Explicit Plans to Guide Inductive Proofs. 111-120
• 
  D. Duchier, Drew V. McDermott: LOGICALC: An Environment for Interactive Proof Development. 121-130

Session 4

• 
  Maritta Heisel, Wolfgang Reif, Werner Stephan: Implementing Verification Strategies in the KIV-System. 131-140
• 
  Donald Simon: Checking Natural Language Proofs. 141-150
• 
  Marc Bezem: Consistency of Rule-based Expert System. 151-161

Session 5

• 
  Hantao Zhang, Deepak Kapur, Mukkai S. Krishnamoorthy: A Mechanizable Induction Principle for Equational Specifications. 162-181
• 
  Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder: Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time. 182-196

Session 6

• 
  Michael A. McRobbie, Robert K. Meyer, Paul B. Thistlewaite: Towards Efficient "Knowledge-Based" Automated Theorem Proving for Non-Standard Logics. 197-217
• 
  A. A. Aaby, K. T. Narayana: Propositional Temporal Interval Logic is PSPACE Complete. 218-237

Session 7

• 
  Douglas J. Howe: Computational Metatheory in Nuprl. 238-257
• 
  H. Azzoune: Type Inference in Prolog. 258-277

Session 8

• 
  Jack Minker, Arcot Rajasekar: Procedural Interpretation of Non-Horn Logic Programs. 278-293
• 
  Shan Chi, Lawrence J. Henschen: Recursive Query Answering with Non-Horn Clauses. 294-312

Session 9

• 
  Toshiro Wakayama, T. H. Payne: Case Inference in Resolution-Based Languages. 313-322
• 
  Ralph Butler, Rasiah Loganantharaj, Robert Olson: Notes on Prolog Program Transformations, Prolog Style, and Efficient Compilation to The Warren Abstract Machine. 323-332
• 
  Ralph Butler, Nicholas T. Karonis: Exploitation of Parallelism in Prototypical Deduction Problems. 333-343

Session 10

• 
  Louise E. Moser: A Decision Procedure for Unquantified Formulas of Graph Theory. 344-357
• 
  Patrick Lincoln, Jim Christian: Adventures in Associative-Commutative Unification (A Summary). 358-367
• 
  Wolfram Büttner: Unification in Finite Algebras is Unitary (?). 368-377

Session 11

• 
  Manfred Schmidt-Schauß: Unification in a Combination of Arbitrary Disjoint Equational Theories. 378-396
• 
  Karl-Hans Bläsius, Jörg H. Siekmann: Partial Unification for Graph Based Equational Reasoning. 397-414

Session 12

• 
  Rainer Manthey, François Bry: SATCHMO: A Theorem Prover Implemented in Prolog. 415-434
• 
  Richard C. Potter, David A. Plaisted: Term Rewriting: Some Experimental Results. 435-453

Session 13

• 
  Bishop Brock, Shaun Cooper, William Pierce: Analogical Reasoning and Proof Discovery. 454-468
• 
  Larry M. Hines: Hyper-Chaining and Knowledge-Based Theorem Proving. 469-486

Session 14

• 
  Luis Fariñas del Cerro, Andreas Herzig: Linear Modal Deductions. 487-499
• 
  Hans Jürgen Ohlbach: A Resolution Calculus for Modal Logics. 500-516

Session 15

• 
  Hans-Jürgen Bürckert: Solving Disequations in Equational Theories. 517-526
• 
  Emmanuel Kounalis, Michaël Rusinowitch: On Word Problems in Horn Theories. 527-537
• 
  Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar: Canonical Conditional Rewrite Systems. 538-549
• 
  Paul Jacquet: Program Synthesis by Completion with Dependent Subtypes. 550-562

Session 16

• 
  Thomas Käufl: Reasoning about Systems of Linear Inequalities. 563-572
• 
  Rolf Socher: A Subsumption Algorithm Based on Characteristic Matrices. 573-581
• 
  Arkady Rabinov: A Restriction of Factoring in Binary Resolution. 582-591
• 
  Philippe Besnard, Pierre Siegel: Supposition-Based Logic for Automated Nonmontonic Reasoning. 592-601

Session 17

• 
  Christoph Walther: Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. 602-621
• 
  Leo Marcus, Timothy Redmond: Two Automated Methods in Implementation Proofs. 622-642

Session 18

• 
  Mark Franzen, Lawrence J. Henschen: A New Approach to Universal Unification and Its Application to AC-Unification. 643-657
• 
  Neil V. Murray, Erik Rosenthal: An Implementation of a Dissolution-Based System Employing Theory Links. 658-674

Session 19

• 
  Ilkka Niemelä: Decision Procedure for Autoepistemic Logic. 675-684
• 
  Peter K. Malkin, Errol P. Martin: Logical Matrix Generation and Testing. 685-693
• 
  Rakesh M. Verma, I. V. Ramakrishnan: Optimal Time Bounds for Parallel Term Matching. 694-703

Session 20

• 
  William McCune: Challenge Equality Problems in Lattice Theory. 704-709
• 
  Frank Pfenning: Single Axioms in the Implicational Propositional Calculus. 710-713
• 
  Larry Wos, William McCune: Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. 714-729
• 
  Rick L. Stevens: Challenge Problems from Nonassociative Rings for Theorem Provers. 730-734

System Abstracts

• 
  Matt Kaufmann: An Interactive Enhancement to the Boyer-Moore Theorem Prover. 735-736
• 
  David A. Plaisted: A Goal Directed Theorem Prover. 737
• 
  Bill Pase, Sentot Kromodimoeljo: m-NEVER System Summary. 738-739
• 
  Timothy Griffin: EFS - An Interactive Environment for Formal Systems. 740-741
• 
  David A. McAllester: Ontic: A Knowledge Representation System for Mathematics. 742-743
• 
  Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade: Some Tools for an Inference Laboratory (ATINF). 744-745
• 
  V. S. Subrahmanian, Zerksis D. Umrigar: QUANTLOG: A System for Approximate Reasoning in Inconsistent Formal Systems. 746-747
• 
  Stephen J. Garland, John V. Guttag: LP: The Larch Prover. 748-749
• 
  Mark E. Stickel: The KLAUS Automated Deduction System. 750-751
• 
  Mark E. Stickel: A Prolog Technology Theorem Prover. 752-753
• 
  Amy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov: Lambda-Prolog: An Extended Logic Programming Language. 754-755
• 
  Frank M. Brown, Seung S. Park: SYMEVAL: A Theorem Prover Based on the Experimental Logic. 756-757
• 
  Frank M. Brown, Seung S. Park, Jim Phelps: ZPLAN: An Automatic Reasoning System for Situations. 758-759
• 
  Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning: The TPS Theorem Proving System. 760-761
• 
  Pierre Bieber, Luis Fariñas del Cerro, Andreas Herzig: MOLOG: a Modal PROLOG. 762-763
• 
  P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. 764-765
• 
  Bruce T. Smith, Donald W. Loveland: An nH-Prolog Implementation. 766-767
• 
  Deepak Kapur, Hantao Zhang: RRL: A Rewrite Rule Laboratory. 768-769
• 
  David Cyrluk, Richard M. Harris, Deepak Kapur: GEOMETER: A Theorem Prover for Algebraic Geometry. 770-771
• 
  Lawrence C. Paulson: Isabelle: The Next Seven Hundred Theorem Provers. 772-773
• 
  Mehmet Dincbas, Pascal Van Hentenryck, Helmut Simonis, Abderrahmane Aggoun, Alexander Herold: The CHIP System: Constraint Handling In Prolog. 774-775