Abstract is missing.
- Connections and Higher-Order LogicPeter B. Andrews. 1-4
- Commutation, Transformation, and TerminationLeo Bachmair, Nachum Dershowitz. 5-20
- Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting SystemsSara Porat, Nissim Francez. 21-41
- An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial InterpretationsAhlem Ben Cherifa, Pierre Lescanne. 42-51
- Proving Termination of Associative Commutative Rewriting Systems by RewritingIsabelle Gnaedig, Pierre Lescanne. 52-61
- Relating Resolution and Algebraic Completion for Horn LogicRoland Dietrich. 62-78
- A Simple Non-Termination Test for the Knuth-Bendix MethodDavid A. Plaisted. 79-88
- A New Formula for the Execution of Categorial CombinatorsRafael Dueire Lins. 89-98
- Proof by Induction Using Test SetsDeepak Kapur, Paliath Narendran, Hantao Zhang. 99-117
- How to Prove Equivalence of Term Rewriting Systems without InductionYoshihito Toyama. 118-127
- Sufficient Completness, Term Rewriting Systems and Anti-Unification Hubert Comon. 128-140
- A New Method for Establishing Refutational Completeness in Theorem ProvingJieh Hsiang, Michaël Rusinowitch. 141-152
- Some Contributions to the Logical Analysis of CircumscritionGerhard Jäger. 154-171
- Modal Theorem ProvingMartín Abadi, Zohar Manna. 172-189
- Computational Aspects of Three-Valued LogicPeter H. Schmitt. 190-198
- Resolution and Quantified Epistemic LogicsKurt Konolige. 199-208
- A Commonsense Theory of Nonmonotonic ReasoningFrank M. Brown. 209-228
- Negative ParamodulationLarry Wos, William McCune. 229-239
- The Heuristics and Experimental Results of a New Hyperparamodulation: HL-ResolutionYounghwan Lim. 240-253
- ECR: An Equality Conditional Resolution Proof ProcedureTie-Cheng Wang. 254-271
- Using Narrowing to do Isolation in Symbolic Equation Solving - An Experiment in Automated ReasoningA. J. J. Dick, Jim Cunningham. 272-280
- Formulation of Induction Formulas in Verification of Prolog ProgramsTadashi Kanamori, Hiroshi Fujita. 281-299
- Program Verifier Tatzelwurm : Reasoning about Systems of Linear InequalitiesThomas Käufl. 300-305
- An Interactive Verification System Based on Dynamic LogicReiner Hähnle, Maritta Heisel, Wolfgang Reif, Werner Stephan. 306-315
- What You Always Wanted to Know About Clause Graph ResolutionNorbert Eisinger. 316-336
- Parallel Theorem Proving with Connection GraphsRasiah Loganantharaj, Robert A. Mueller. 337-352
- Theory Links in Semantic GraphsNeil V. Murray, Erik Rosenthal. 353-364
- Abstraction Using Generalization FunctionsDavid A. Plaisted. 365-376
- An Improvement of Deduction Plans: Refutation PlansHans-Albert Schneider. 377-383
- Controlling Deduction with Proof Condensation and HeuristicsFranz Oppacher, E. Suen. 384-393
- Nested ResolutionJonathan Traugott. 394-402
- Mechanizing Constructive Proofs (Abstract)Gérard P. Huet. 403
- Implementing Number Theory: An Experiment with NuprlDouglas J. Howe. 404-415
- Parallel Algorithms for Term MatchingCynthia Dwork, Paris C. Kanellakis, Larry J. Stockmeyer. 416-430
- Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function SymbolsErik Tidén. 431-449
- Combination of Unification AlgorithmsAlexander Herold. 450-469
- Unification in the Data Structure SetsWolfram Büttner. 470-488
- NP-Completeness of the Set Unification and Matching ProblemsDeepak Kapur, Paliath Narendran. 489-495
- Matching with DistributivityJalel Mzali. 496-505
- Unification in Boolean RingsUrsula Martin, Tobias Nipkow. 506-513
- Some Relationships between Unification, restricted Unification, and MatchingHans-Jürgen Bürckert. 514-524
- A Classification of Many-Sorted Unification ProblemsChristoph Walther. 525-537
- Unification in Many-Sorted Eqational TheoriesManfred Schmidt-Schauß. 538-552
- Classes of First Order Formulas Under Various Satisfiability DefinitionsHans Kleine Büning, Theodor Lettmann. 553-563
- Diamond Formulas in the Dynamic Logic of Recursively Enumerable ProgramsVolker Weispfenning. 564-571
- A prolog Technology Theorem Prover: Implementation by an Extended Prolog CompilerMark E. Stickel. 573-587
- Paths to High-Performance Automated Theorem ProvingRalph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek. 588-597
- Purely Functional Implementation of a LogicF. Keith Hanna, Neil Daeche. 598-607
- Causes for Events: Their Computation and ApplicationsPhilip T. Cox, Tomasz Pietrzykowski. 608-621
- How to Clear a Block: Plan Formation in Situational LogicZohar Manna, Richard J. Waldinger. 622-640
- Deductive Synthesis of Sorting ProgramsJonathan Traugott. 641-660
- The TPS Theorem Proving SystemPeter B. Andrews, Frank Pfenning, Sunil Issar, C. P. Klapper. 663-664
- TRSPEC: A Term Rewriting Based System for Algebraic SpecificationsJürgen Avenhaus, Benjamin Benninghofen, Rüdiger Göbel, Klaus Madlener. 665-667
- Highly Parallel Inference MachineM. Bayerl. 668-669
- Automatic Theorem Proving in the ISDV SystemChristoph Beierle, Walter G. Olthoff, Angi Voß. 670-671
- The Karlsruhe Induction Theorem Proving SystemSusanne Biundo, B. Hummel, Dieter Hutter, Christoph Walther. 672-674
- Overview of a Theorem-Prover for A Computational LogicRobert S. Boyer, J. Strother Moore. 675-678
- GEO-Prover - A Geometry Theorem Prover Developed at UTShang-Ching Chou. 679-680
- The Markgraf Karl Refutation Procedure (MKRP)Norbert Eisinger, Hans Jürgen Ohlbach. 681-682
- The J-Machine: Functional Programming with CombinatorsJacek Gibert. 683-684
- The Illinois Prover: A General Purpose Resolution Theorem ProverSteven Greenbaum, David A. Plaisted. 685-687
- Theorem Proving Systems of the Formel ProjectGérard P. Huet. 687-688
- The Passau RAP System: Prototyping Algebraic Specifications Using Conditional NarrowingHeinrich Hußmann. 689-690
- RRL: A Rewrite Rule LaboratoryDeepak Kapur, G. Sivakumar, Hantao Zhang. 691-692
- A Geometry Theorem Prover Based on Buchberger s AlgorithmB. Kutzler, Sabine Stifter. 693-694
- REVE a Rewrite Rule LaboratoryPierre Lescanne. 695-696
- ITP at Argonne National LaboratoryEwing L. Lusk, William McCune, Ross A. Overbeek. 697-698
- AUTOLOGIC at University of VictoriaCharles G. Morgan. 699-700
- THINKERFrancis Jeffry Pelletier. 701-702
- The KLAUS Automated Deduction SystemMark E. Stickel. 703-704
- The KRIPKE Automated Theorem Proving SystemPaul B. Thistlewaite, Michael A. McRobbie, Robert K. Meyer. 705-706
- SHD-Prover at University of Texas at AustinTie-Cheng Wang. 707-708