Abstract is missing.
- A Theorem Prover for a Computational LogicRobert S. Boyer, J. Strother Moore. 1-15
- A Complete Semantic Back Chaining Proof SystemXumin Nie, David A. Plaisted. 16-27
- Parallelizing the Closure Computation in Automated DeductionJohn K. Slaney, Ewing L. Lusk. 28-39
- PARTHEO: A High-Performance Parallel Theorem ProverJohann Schumann, Reinhold Letz. 40-56
- Substitution-based Compilation of Extended Rules in Deductive DatabasesSang Ho Lee, Lawrence J. Henschen. 57-71
- Automatic Theorem Proving in Paraconsistent Logics: Theory and ImplementationNewton C. A. da Costa, Lawrence J. Henschen, James J. Lu, V. S. Subrahmanian. 72-86
- Case-Free Programs: An Abstraction of Definite Horn ProgramsToshiro Wakayama, T. H. Payne. 87-101
- Generalized Well-founded Semantics for Logic Programs (Extended Abstract)Chitta Baral, Jorge Lobo, Jack Minker. 102-116
- Tactical Theorem Proving in Program VerificationMaritta Heisel, Wolfgang Reif, Werner Stephan. 117-131
- Extensions to the Rippling-Out Tactic for Guiding Inductive ProofsAlan Bundy, Frank van Harmelen, Alan Smaill, Andrew Ireland. 132-146
- Guiding Induction ProofsDieter Hutter. 147-161
- Term Rewriting InductionUday S. Reddy. 162-177
- A Resolution Principle for Clauses with ConstraintsHans-Jürgen Bürckert. 178-192
- Str+ve-Subset: The Str+ve-based Subset ProverLarry M. Hines. 193-206
- Ritt-Wu s Decomposition Algorithm and Geometry Theorem ProvingShang-Ching Chou, Xiao-Shan Gao. 207-220
- Encoding a Dependent-Type Lambda-Calculus in a Logic Programming LanguageAmy P. Felty, Dale Miller. 221-235
- Investigations into Proof-Search in a System of First-Order Dependent Function TypesDavid J. Pym, Lincoln A. Wallen. 236-250
- Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism CompleteDavid A. Basin. 251-260
- An Improved General E-Unification MethodDaniel J. Dougherty, Patricia Johann. 261-275
- Some Results on Equational UnificationPaliath Narendran, Friedrich Otto. 276-291
- Unification in a Combination of Equational Theories: an Efficient AlgorithmAlexandre Boudet. 292-307
- SLIM: An Automated Reasoner For Equivalences, Applied To Set TheoryAlan F. McMichael. 308-321
- An Examination of the Prolog Technology Theorem-ProverMark Tarver. 322-335
- Presenting Intuitive Deductions via Symmetric SimplificationFrank Pfenning, Dan Nesmith. 336-350
- Toward Mechanical Methods for Streamlining ProofsWilliam Pierce. 351-365
- Ordered Rewriting and ConfluenceUrsula Martin, Tobias Nipkow. 366-380
- Complete Sets of Reductions with ConstraintsGerald E. Peterson. 381-395
- Rewrite Systems for Varieties of SemigroupsFranz Baader. 396-410
- Improving Assoviative Path OrderingsJoachim Steinbach. 411-425
- Perspectives on Automated Deduction (Abstract)Wolfgang Bibel. 426
- On Restrictions of Ordered Paramodulation with SimplificationLeo Bachmair, Harald Ganzinger. 427-441
- Simultaneous ParamodulationDan Benanav. 442-455
- Hyper Resolution and Equality Axioms without Function SubstitutionsYusuf Ozturk, Lawrence J. Henschen. 456-469
- Automatic Acquisition of Search Guiding HeuristicsChristian B. Suttner, Wolfgang Ertel. 470-484
- Automated Reasoning Contributed to Mathematics and LogicLarry Wos, S. Winker, William McCune, Ross A. Overbeek, Ewing L. Lusk, Rick L. Stevens, Ralph Butler. 485-499
- A Mechanically Assisted Constructive Proof in Category TheoryJames A. Altucher, Prakash Panangaden. 500-513
- Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional LogicHeikki Tuominen. 514-527
- A Tableau-Based Theorem Prover for a Decidable Subset of Default LogicCamilla Schwind. 528-542
- Computing Prime ImplicantsPeter Jackson, John Pais. 543-557
- Minimizing the Number of Clauses by RenamingThierry Boy de la Tour. 558-572
- Higher Order E-UnificationWayne Snyder. 573-587
- Programming by Example and Proving by Example Using Higher-order UnificationMasami Hagiya. 588-602
- Retrieving Library Identifiers via Equational Matching of TypesMikael Rittri. 603-617
- Unification in Monoidal TheoriesWerner Nutt. 618-632
- A Science of Reasoning: Extended AbstractAlan Bundy. 633-640
- The TPS Theorem Proving SystemPeter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning. 641-642
- SchemataFrank M. Brown, Carlos Araya. 643-644
- Cylindric Algebra Equation SolverFrank M. Brown, Carlos Araya. 645-646
- The Oyster-Clam SystemAlan Bundy, Frank van Harmelen, Christian Horn, Alan Smaill. 647-648
- A High-Performance Parallel Theorem ProverRalph Butler, Ian T. Foster, Anita Jindal, Ross A. Overbeek. 649-650
- The Romulus Proof CheckerCarl Eichenlaub, Bruce Esrig, James Hook, Carl Klapper, Garrel Pottinger. 651-652
- IMPS: An Interactive Mathematical Proof SystemWilliam M. Farmer, Joshua D. Guttman, F. Javier Thayer. 653-654
- UNICOM: A Refined Completion Based Inductive Theorem ProverBernhard Gramlich. 655-656
- The Theorem Prover of the Program Verifier TatzelwurmThomas Käufl, Nicolas Zabel. 657-658
- RCL: A Lisp Verification SystemMatt Kaufmann. 659-660
- ORME: An Implementation of Completion Procedures as Sets of Transition RulesPierre Lescanne. 661-662
- OTTER 2.0William McCune. 663-664
- DISSOLVER: A Dissolution-based Theorem ProverNeil V. Murray, Erik Rosenthal. 665-666
- TRIP: An Implementation of Clausal RewritingRobert Nieuwenhuis, Fernando Orejas, Albert Rubio. 667-668
- OSCARJohn L. Pollock. 669-670
- EXPERT THINKER: An Adaptation of F-Prolog to MicrocomputersRonald W. Satz. 671-672
- A Prolog Technology Theorem ProverMark E. Stickel. 673-674
- A General Clause Theorem ProverGeoff Sutcliffe. 675-676
- LISS - The Logic Inference Search SystemAndrei Voronkov. 677-678
- ACE: The Abstract Clause EngineDavid A. Wolfram. 679-680
- Tutorial on Reasoning and Representation with Concept LanguagesJürgen Müller, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka. 681
- Tutorial on High-Performance Automated Theorem ProvingEwing L. Lusk, William McCune. 681
- Tutorial on Equational UnificationClaude Kirchner. 682
- Tutorial on Lambda-PrologAmy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning. 682
- Tutorial on Compilation techniques for LogicsHans Jürgen Ohlbach, Andreas Herzig. 683
- Tutorial on High-Performance Theorem Provers: Efficient Implementation and ParallelisationJohann Schumann, Reinhold Letz, Franz J. Kurfess. 683
- Tutorial on Program-Synthetic DeductionRichard J. Waldinger. 684
- Tutorial on Rewrite-Based Theorem ProvingJieh Hsiang, Jean-Pierre Jouannaud. 684
- Tutorial on Computing Models of Propositional LogicsPaul Pritchard, John K. Slaney. 685