8. CADE 1986: Oxford, England

Invited Talk

• Peter B. Andrews:
  Connections and Higher-Order Logic. 1-4
  

Term Rewriting Systems

• Leo Bachmair, Nachum Dershowitz:
  Commutation, Transformation, and Termination. 5-20
  
• Sara Porat, Nissim Francez:
  Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems. 21-41
  
• Ahlem Ben Cherifa, Pierre Lescanne:
  An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations. 42-51
  
• Isabelle Gnaedig, Pierre Lescanne:
  Proving Termination of Associative Commutative Rewriting Systems by Rewriting. 52-61
  
• Roland Dietrich:
  Relating Resolution and Algebraic Completion for Horn Logic. 62-78
  
• David A. Plaisted:
  A Simple Non-Termination Test for the Knuth-Bendix Method. 79-88
  
• Rafael Dueire Lins:
  A New Formula for the Execution of Categorial Combinators. 89-98
  
• Deepak Kapur, Paliath Narendran, Hantao Zhang:
  Proof by Induction Using Test Sets. 99-117
  
• Yoshihito Toyama:
  How to Prove Equivalence of Term Rewriting Systems without Induction. 118-127
  
• Hubert Comon:
  Sufficient Completness, Term Rewriting Systems and "Anti-Unification". 128-140
  
• Jieh Hsiang, Michaël Rusinowitch:
  A New Method for Establishing Refutational Completeness in Theorem Proving. 141-152
  

Nonclassical Deduction

• Gerhard Jäger:
  Some Contributions to the Logical Analysis of Circumscrition. 154-171
  
• Martín Abadi, Zohar Manna:
  Modal Theorem Proving. 172-189
  
• Peter H. Schmitt:
  Computational Aspects of Three-Valued Logic. 190-198
  
• Kurt Konolige:
  Resolution and Quantified Epistemic Logics. 199-208
  
• Frank M. Brown:
  A Commonsense Theory of Nonmonotonic Reasoning. 209-228
  

Equality Reasoning

• Larry Wos, William McCune:
  Negative Paramodulation. 229-239
  
• Younghwan Lim:
  The Heuristics and Experimental Results of a New Hyperparamodulation: HL-Resolution. 240-253
  
• Tie-Cheng Wang:
  ECR: An Equality Conditional Resolution Proof Procedure. 254-271
  
• A. J. J. Dick, Jim Cunningham:
  Using Narrowing to do Isolation in Symbolic Equation Solving - An Experiment in Automated Reasoning. 272-280
  

Program Verification

• Tadashi Kanamori, Hiroshi Fujita:
  Formulation of Induction Formulas in Verification of Prolog Programs. 281-299
  
• Thomas Käufl:
  Program Verifier "Tatzelwurm": Reasoning about Systems of Linear Inequalities. 300-305
  
• Reiner Hähnle, Maritta Heisel, Wolfgang Reif, Werner Stephan:
  An Interactive Verification System Based on Dynamic Logic. 306-315
  

Graph Based Deduction

• Norbert Eisinger:
  What You Always Wanted to Know About Clause Graph Resolution. 316-336
  
• Rasiah Loganantharaj, Robert A. Mueller:
  Parallel Theorem Proving with Connection Graphs. 337-352
  
• Neil V. Murray, Erik Rosenthal:
  Theory Links in Semantic Graphs. 353-364
  

Special Deduction Systems

• David A. Plaisted:
  Abstraction Using Generalization Functions. 365-376
  
• Hans-Albert Schneider:
  An Improvement of Deduction Plans: Refutation Plans. 377-383
  
• Franz Oppacher, E. Suen:
  Controlling Deduction with Proof Condensation and Heuristics. 384-393
  
• Jonathan Traugott:
  Nested Resolution. 394-402
  

Invited Talk

• Gérard P. Huet:
  Mechanizing Constructive Proofs (Abstract). 403
  

Constructive ATP

• Douglas J. Howe:
  Implementing Number Theory: An Experiment with Nuprl. 404-415
  

Unification Theory

• Cynthia Dwork, Paris C. Kanellakis, Larry J. Stockmeyer:
  Parallel Algorithms for Term Matching. 416-430
  
• Erik Tidén:
  Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols. 431-449
  
• Alexander Herold:
  Combination of Unification Algorithms. 450-469
  
• Wolfram Büttner:
  Unification in the Data Structure Sets. 470-488
  
• Deepak Kapur, Paliath Narendran:
  NP-Completeness of the Set Unification and Matching Problems. 489-495
  
• Jalel Mzali:
  Matching with Distributivity. 496-505
  
• Ursula Martin, Tobias Nipkow:
  Unification in Boolean Rings. 506-513
  
• Hans-Jürgen Bürckert:
  Some Relationships between Unification, restricted Unification, and Matching. 514-524
  
• Christoph Walther:
  A Classification of Many-Sorted Unification Problems. 525-537
  
• Manfred Schmidt-Schauß:
  Unification in Many-Sorted Eqational Theories. 538-552
  

Theoretical Issues

• Hans Kleine Büning, Theodor Lettmann:
  Classes of First Order Formulas Under Various Satisfiability Definitions. 553-563
  
• Volker Weispfenning:
  Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs. 564-571
  

Logic Programming Oriented Deduction Systems

• Mark E. Stickel:
  A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. 573-587
  
• Ralph Butler, Ewing L. Lusk, William McCune, Ross A. Overbeek:
  Paths to High-Performance Automated Theorem Proving. 588-597
  
• F. Keith Hanna, Neil Daeche:
  Purely Functional Implementation of a Logic. 598-607
  

Deductive Databases, Planning, Synthesis

• Philip T. Cox, Tomasz Pietrzykowski:
  Causes for Events: Their Computation and Applications. 608-621
  
• Zohar Manna, Richard J. Waldinger:
  How to Clear a Block: Plan Formation in Situational Logic. 622-640
  
• Jonathan Traugott:
  Deductive Synthesis of Sorting Programs. 641-660
  

Extended Abstracts of Courrent Deduction Systems

• Peter B. Andrews, Frank Pfenning, Sunil Issar, C. P. Klapper:
  The TPS Theorem Proving System. 663-664
  
• Jürgen Avenhaus, Benjamin Benninghofen, Rüdiger Göbel, Klaus Madlener:
  TRSPEC: A Term Rewriting Based System for Algebraic Specifications. 665-667
  
• M. Bayerl:
  Highly Parallel Inference Machine. 668-669
  
• Christoph Beierle, Walter G. Olthoff, Angi Voß:
  Automatic Theorem Proving in the ISDV System. 670-671
  
• Susanne Biundo, B. Hummel, Dieter Hutter, Christoph Walther:
  The Karlsruhe Induction Theorem Proving System. 672-674
  
• Robert S. Boyer, J. Strother Moore:
  Overview of a Theorem-Prover for A Computational Logic. 675-678
  
• Shang-Ching Chou:
  GEO-Prover - A Geometry Theorem Prover Developed at UT. 679-680
  
• Norbert Eisinger, Hans Jürgen Ohlbach:
  The Markgraf Karl Refutation Procedure (MKRP). 681-682
  
• Jacek Gibert:
  The J-Machine: Functional Programming with Combinators. 683-684
  
• Steven Greenbaum, David A. Plaisted:
  The Illinois Prover: A General Purpose Resolution Theorem Prover. 685-687
  
• Gérard P. Huet:
  Theorem Proving Systems of the Formel Project. 687-688
  
• Heinrich Hußmann:
  The Passau RAP System: Prototyping Algebraic Specifications Using Conditional Narrowing. 689-690
  
• Deepak Kapur, G. Sivakumar, Hantao Zhang:
  RRL: A Rewrite Rule Laboratory. 691-692
  
• B. Kutzler, Sabine Stifter:
  A Geometry Theorem Prover Based on Buchberger's Algorithm. 693-694
  
• Pierre Lescanne:
  REVE a Rewrite Rule Laboratory. 695-696
  
• Ewing L. Lusk, William McCune, Ross A. Overbeek:
  ITP at Argonne National Laboratory. 697-698
  
• Charles G. Morgan:
  AUTOLOGIC at University of Victoria. 699-700
  
• Francis Jeffry Pelletier:
  THINKER. 701-702
  
• Mark E. Stickel:
  The KLAUS Automated Deduction System. 703-704
  
• Paul B. Thistlewaite, Michael A. McRobbie, Robert K. Meyer:
  The KRIPKE Automated Theorem Proving System. 705-706
  
• Tie-Cheng Wang:
  SHD-Prover at University of Texas at Austin. 707-708