Abstract is missing.
- First-Order Theorem Proving Using Conditional Rewrite RulesHantao Zhang, Deepak Kapur. 1-20
- Elements of Z-Module ReasoningTie-Cheng Wang. 21-40
- Learning and Applying Generalised Solutions using Higher Order ResolutionMichael R. Donat, Lincoln A. Wallen. 41-60
- Specifying Theorem Provers in a Higher-Order Logic Programming LanguageAmy P. Felty, Dale Miller. 61-80
- Query Processing in Quantitative Logic ProgrammingV. S. Subrahmanian. 81-100
- An Environment For Automated Reasoning About Partial FunctionsDavid A. Basin. 101-110
- The Use of Explicit Plans to Guide Inductive ProofsAlan Bundy. 111-120
- LOGICALC: An Environment for Interactive Proof DevelopmentD. Duchier, Drew V. McDermott. 121-130
- Implementing Verification Strategies in the KIV-SystemMaritta Heisel, Wolfgang Reif, Werner Stephan. 131-140
- Checking Natural Language ProofsDonald Simon. 141-150
- Consistency of Rule-based Expert SystemMarc Bezem. 151-161
- A Mechanizable Induction Principle for Equational SpecificationsHantao Zhang, Deepak Kapur, Mukkai S. Krishnamoorthy. 162-181
- Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial TimeJean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder. 182-196
- Towards Efficient Knowledge-Based Automated Theorem Proving for Non-Standard LogicsMichael A. McRobbie, Robert K. Meyer, Paul B. Thistlewaite. 197-217
- Propositional Temporal Interval Logic is PSPACE CompleteA. A. Aaby, K. T. Narayana. 218-237
- Computational Metatheory in NuprlDouglas J. Howe. 238-257
- Type Inference in PrologH. Azzoune. 258-277
- Procedural Interpretation of Non-Horn Logic ProgramsJack Minker, Arcot Rajasekar. 278-293
- Recursive Query Answering with Non-Horn ClausesShan Chi, Lawrence J. Henschen. 294-312
- Case Inference in Resolution-Based LanguagesToshiro Wakayama, T. H. Payne. 313-322
- Notes on Prolog Program Transformations, Prolog Style, and Efficient Compilation to The Warren Abstract MachineRalph Butler, Rasiah Loganantharaj, Robert Olsen. 323-332
- Exploitation of Parallelism in Prototypical Deduction ProblemsRalph Butler, Nicholas T. Karonis. 333-343
- A Decision Procedure for Unquantified Formulas of Graph TheoryLouise E. Moser. 344-357
- Adventures in Associative-Commutative Unification (A Summary)Patrick Lincoln, Jim Christian. 358-367
- Unification in Finite Algebras is Unitary (?)Wolfram Büttner. 368-377
- Unification in a Combination of Arbitrary Disjoint Equational TheoriesManfred Schmidt-Schauß. 378-396
- Partial Unification for Graph Based Equational ReasoningKarl-Hans Bläsius, Jörg H. Siekmann. 397-414
- SATCHMO: A Theorem Prover Implemented in PrologRainer Manthey, François Bry. 415-434
- Term Rewriting: Some Experimental ResultsRichard C. Potter, David A. Plaisted. 435-453
- Analogical Reasoning and Proof DiscoveryBishop Brock, Shaun Cooper, William Pierce. 454-468
- Hyper-Chaining and Knowledge-Based Theorem ProvingLarry M. Hines. 469-486
- Linear Modal DeductionsLuis Fariñas del Cerro, Andreas Herzig. 487-499
- A Resolution Calculus for Modal LogicsHans Jürgen Ohlbach. 500-516
- Solving Disequations in Equational TheoriesHans-Jürgen Bürckert. 517-526
- On Word Problems in Horn TheoriesEmmanuel Kounalis, Michaël Rusinowitch. 527-537
- Canonical Conditional Rewrite SystemsNachum Dershowitz, Mitsuhiro Okada, G. Sivakumar. 538-549
- Program Synthesis by Completion with Dependent SubtypesPaul Jacquet. 550-562
- Reasoning about Systems of Linear InequalitiesThomas Käufl. 563-572
- A Subsumption Algorithm Based on Characteristic MatricesRolf Socher. 573-581
- A Restriction of Factoring in Binary ResolutionArkady Rabinov. 582-591
- Supposition-Based Logic for Automated Nonmontonic ReasoningPhilippe Besnard, Pierre Siegel. 592-601
- Argument-Bounded Algorithms as a Basis for Automated Termination ProofsChristoph Walther. 602-621
- Two Automated Methods in Implementation ProofsLeo Marcus, Timothy Redmond. 622-642
- A New Approach to Universal Unification and Its Application to AC-UnificationMark Franzen, Lawrence J. Henschen. 643-657
- An Implementation of a Dissolution-Based System Employing Theory LinksNeil V. Murray, Erik Rosenthal. 658-674
- Decision Procedure for Autoepistemic LogicIlkka Niemelä. 675-684
- Logical Matrix Generation and TestingPeter K. Malkin, Errol P. Martin. 685-693
- Optimal Time Bounds for Parallel Term MatchingRakesh M. Verma, I. V. Ramakrishnan. 694-703
- Challenge Equality Problems in Lattice TheoryWilliam McCune. 704-709
- Single Axioms in the Implicational Propositional CalculusFrank Pfenning. 710-713
- Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving ProgramsLarry Wos, William McCune. 714-729
- Challenge Problems from Nonassociative Rings for Theorem ProversRick L. Stevens. 730-734
- An Interactive Enhancement to the Boyer-Moore Theorem ProverMatt Kaufmann. 735-736
- A Goal Directed Theorem ProverDavid A. Plaisted. 737
- m-NEVER System SummaryBill Pase, Sentot Kromodimoeljo. 738-739
- EFS - An Interactive Environment for Formal SystemsTimothy Griffin. 740-741
- Ontic: A Knowledge Representation System for MathematicsDavid A. McAllester. 742-743
- Some Tools for an Inference Laboratory (ATINF)Thierry Boy de la Tour, Ricardo Caferra, Gilles Chaminade. 744-745
- QUANTLOG: A System for Approximate Reasoning in Inconsistent Formal SystemsV. S. Subrahmanian, Zerksis D. Umrigar. 746-747
- LP: The Larch ProverStephen J. Garland, John V. Guttag. 748-749
- The KLAUS Automated Deduction SystemMark E. Stickel. 750-751
- A Prolog Technology Theorem ProverMark E. Stickel. 752-753
- Lambda-Prolog: An Extended Logic Programming LanguageAmy P. Felty, Elsa L. Gunter, John Hannan, Dale Miller, Gopalan Nadathur, Andre Scedrov. 754-755
- SYMEVAL: A Theorem Prover Based on the Experimental LogicFrank M. Brown, Seung S. Park. 756-757
- ZPLAN: An Automatic Reasoning System for SituationsFrank M. Brown, Seung S. Park, Jim Phelps. 758-759
- The TPS Theorem Proving SystemPeter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning. 760-761
- MOLOG: a Modal PROLOGPierre Bieber, Luis Fariñas del Cerro, Andreas Herzig. 762-763
- PARTHENON: A Parallel Theorem Prover for Non-Horn ClausesP. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov. 764-765
- An nH-Prolog ImplementationBruce T. Smith, Donald W. Loveland. 766-767
- RRL: A Rewrite Rule LaboratoryDeepak Kapur, Hantao Zhang. 768-769
- GEOMETER: A Theorem Prover for Algebraic GeometryDavid Cyrluk, Richard M. Harris, Deepak Kapur. 770-771
- Isabelle: The Next Seven Hundred Theorem ProversLawrence C. Paulson. 772-773
- The CHIP System: Constraint Handling In PrologMehmet Dincbas, Pascal Van Hentenryck, Helmut Simonis, Abderrahmane Aggoun, Alexander Herold. 774-775