## Jörg H. Siekmann

*Proceedings of the Eighth International Conference on Automated Deduction*

CADE, 1986.

@proceedings{CADE-1986, editor = "Jörg H. Siekmann", isbn = "3-540-16780-3", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Eighth International Conference on Automated Deduction}", volume = 230, year = 1986, }

### Contents (72 items)

- CADE-1986-Andrews #higher-order #logic
- Connections and Higher-Order Logic (PBA), pp. 1–4.
- CADE-1986-BachmairD #termination
- Commutation, Transformation, and Termination (LB, ND), pp. 5–20.
- CADE-1986-PoratF #equation #term rewriting
- Full-Commutation and Fair-Termination in Equational (and Combined) Term-Rewriting Systems (SP, NF), pp. 21–41.
- CADE-1986-CherifaL #implementation #polynomial #term rewriting #termination
- An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations (ABC, PL), pp. 42–51.
- CADE-1986-GnaedigL #commutative #proving #term rewriting #termination
- Proving Termination of Associative Commutative Rewriting Systems by Rewriting (IG, PL), pp. 52–61.
- CADE-1986-Dietrich #algebra #logic
- Relating Resolution and Algebraic Completion for Horn Logic (RD), pp. 62–78.
- CADE-1986-Plaisted
- A Simple Non-Termination Test for the Knuth-Bendix Method (DAP), pp. 79–88.
- CADE-1986-Lins #combinator #execution
- A New Formula for the Execution of Categorial Combinators (RDL), pp. 89–98.
- CADE-1986-KapurNZ #induction #proving #testing #using
- Proof by Induction Using Test Sets (DK, PN, HZ), pp. 99–117.
- CADE-1986-Toyama #equivalence #how #induction #term rewriting
- How to Prove Equivalence of Term Rewriting Systems without Induction (YT), pp. 118–127.
- CADE-1986-Comon #anti #term rewriting
- Sufficient Completeness, Term Rewriting Systems and “Anti-Unification” (HC), pp. 128–140.
- CADE-1986-HsiangR #proving #theorem proving
- A New Method for Establishing Refutational Completeness in Theorem Proving (JH, MR), pp. 141–152.
- CADE-1986-Jager #analysis #logic
- Some Contributions to the Logical Analysis of Circumscrition (GJ), pp. 154–171.
- CADE-1986-AbadiM #proving #theorem proving
- Modal Theorem Proving (MA, ZM), pp. 172–189.
- CADE-1986-Schmitt #aspect-oriented #logic
- Computational Aspects of Three-Valued Logic (PHS), pp. 190–198.
- CADE-1986-Konolige #logic #quantifier
- Resolution and Quantified Epistemic Logics (KK), pp. 199–208.
- CADE-1986-Brown #reasoning
- A Commonsense Theory of Nonmonotonic Reasoning (FMB), pp. 209–228.
- CADE-1986-WosM
- Negative Paramodulation (LW, WM), pp. 229–239.
- CADE-1986-Lim #heuristic
- The Heuristics and Experimental Results of a New Hyperparamodulation: HL-Resolution (YL), pp. 240–253.
- CADE-1986-Wang #named #proving #similarity
- ECR: An Equality Conditional Resolution Proof Procedure (TCW), pp. 254–271.
- CADE-1986-DickC #automation #empirical #equation #reasoning #using
- Using Narrowing to do Isolation in Symbolic Equation Solving — An Experiment in Automated Reasoning (AJJD, JC), pp. 272–280.
- CADE-1986-KanamoriF #induction #prolog #source code #verification
- Formulation of Induction Formulas in Verification of Prolog Programs (TK, HF), pp. 281–299.
- CADE-1986-Kafl #linear #reasoning #verification
- Program Verifier “Tatzelwurm”: Reasoning about Systems of Linear Inequalities (TK), pp. 300–305.
- CADE-1986-HahnleHRS #interactive #logic #verification
- An Interactive Verification System Based on Dynamic Logic (RH, MH, WR, WS), pp. 306–315.
- CADE-1986-Eisinger #graph #what
- What You Always Wanted to Know About Clause Graph Resolution (NE), pp. 316–336.
- CADE-1986-LoganantharajM #graph #parallel #proving #theorem proving
- Parallel Theorem Proving with Connection Graphs (RL, RAM), pp. 337–352.
- CADE-1986-MurrayR #graph #semantics
- Theory Links in Semantic Graphs (NVM, ER), pp. 353–364.
- CADE-1986-Plaisted86a #abstraction #using
- Abstraction Using Generalization Functions (DAP), pp. 365–376.
- CADE-1986-Schneider #deduction
- An Improvement of Deduction Plans: Refutation Plans (HAS), pp. 377–383.
- CADE-1986-OppacherS #deduction #heuristic #proving
- Controlling Deduction with Proof Condensation and Heuristics (FO, ES), pp. 384–393.
- CADE-1986-Traugott
- Nested Resolution (JT), pp. 394–402.
- CADE-1986-Huet #proving
- Mechanizing Constructive Proofs (GPH), p. 403.
- CADE-1986-Howe #empirical #implementation
- Implementing Number Theory: An Experiment with Nuprl (DJH), pp. 404–415.
- CADE-1986-DworkCKS #algorithm #parallel
- Parallel Algorithms for Term Matching (CD, PCK, LJS), pp. 416–430.
- CADE-1986-Tiden #set #unification
- Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols (ET), pp. 431–449.
- CADE-1986-Herold #algorithm #unification
- Combination of Unification Algorithms (AH), pp. 450–469.
- CADE-1986-Buttner #data type #set #unification
- Unification in the Data Structure Sets (WB), pp. 470–488.
- CADE-1986-KapurN #problem #set #unification
- NP-Completeness of the Set Unification and Matching Problems (DK, PN), pp. 489–495.
- CADE-1986-Mzali
- Matching with Distributivity (JM), pp. 496–505.
- CADE-1986-MartinN #unification
- Unification in Boolean Rings (UM, TN), pp. 506–513.
- CADE-1986-Burckert #strict #unification
- Some Relationships between Unification, restricted Unification, and Matching (HJB), pp. 514–524.
- CADE-1986-Walther #classification #problem #unification
- A Classification of Many-Sorted Unification Problems (CW), pp. 525–537.
- CADE-1986-Schmidt-Schauss #unification
- Unification in Many-Sorted Eqational Theories (MSS), pp. 538–552.
- CADE-1986-BuningL #first-order #satisfiability
- Classes of First Order Formulas Under Various Satisfiability Definitions (HKB, TL), pp. 553–563.
- CADE-1986-Weispfenning #logic #recursion #source code
- Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs (VW), pp. 564–571.
- CADE-1986-Stickel #compilation #implementation #prolog #proving #theorem proving
- A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler (MES), pp. 573–587.
- CADE-1986-ButlerLMO #automation #proving #theorem proving
- Paths to High-Performance Automated Theorem Proving (RB, ELL, WM, RAO), pp. 588–597.
- CADE-1986-HannaD #functional #implementation #logic
- Purely Functional Implementation of a Logic (FKH, ND), pp. 598–607.
- CADE-1986-CoxP
- Causes for Events: Their Computation and Applications (PTC, TP), pp. 608–621.
- CADE-1986-MannaW #how #logic
- How to Clear a Block: Plan Formation in Situational Logic (ZM, RJW), pp. 622–640.
- CADE-1986-Traugott86a #deduction #sorting #source code #synthesis
- Deductive Synthesis of Sorting Programs (JT), pp. 641–660.
- CADE-1986-AndrewsPIK #proving #theorem proving
- The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.
- CADE-1986-AvenhausBGM #algebra #named #specification #term rewriting
- TRSPEC: A Term Rewriting Based System for Algebraic Specifications (JA, BB, RG, KM), pp. 665–667.
- CADE-1986-Bayerl #parallel
- Highly Parallel Inference Machine (MB), pp. 668–669.
- CADE-1986-BeierleOV #automation #proving #theorem proving
- Automatic Theorem Proving in the ISDV System (CB, WGO, AV), pp. 670–671.
- CADE-1986-BiundoHHW #induction #proving #theorem proving
- The Karlsruhe Induction Theorem Proving System (SB, BH, DH, CW), pp. 672–674.
- CADE-1986-BoyerM #logic #overview
- Overview of a Theorem-Prover for A Computational Logic (RSB, JSM), pp. 675–678.
- CADE-1986-Chou #geometry #named #proving #theorem proving
- GEO-Prover — A Geometry Theorem Prover Developed at UT (SCC), pp. 679–680.
- CADE-1986-EisingerO
- The Markgraf Karl Refutation Procedure (MKRP) (NE, HJO), pp. 681–682.
- CADE-1986-Gibert #combinator #functional #programming
- The J-Machine: Functional Programming with Combinators (JG), pp. 683–684.
- CADE-1986-GreenbaumP #proving #theorem proving
- The Illinois Prover: A General Purpose Resolution Theorem Prover (SG, DAP), pp. 685–687.
- CADE-1986-Huet86a #proving #theorem proving
- Theorem Proving Systems of the Formel Project (GPH), pp. 687–688.
- CADE-1986-Hussmann #algebra #prototype #specification #using
- The Passau RAP System: Prototyping Algebraic Specifications Using Conditional Narrowing (HH), pp. 689–690.
- CADE-1986-KapurSZ #named
- RRL: A Rewrite Rule Laboratory (DK, GS, HZ), pp. 691–692.
- CADE-1986-KutzlerS #algorithm #geometry #proving #theorem proving
- A Geometry Theorem Prover Based on Buchberger’s Algorithm (BK, SS), pp. 693–694.
- CADE-1986-Lescanne
- REVE a Rewrite Rule Laboratory (PL), pp. 695–696.
- CADE-1986-LuskMO
- ITP at Argonne National Laboratory (ELL, WM, RAO), pp. 697–698.
- CADE-1986-Morgan
- AUTOLOGIC at University of Victoria (CGM), pp. 699–700.
- CADE-1986-Pelletier
- THINKER (FJP), pp. 701–702.
- CADE-1986-Stickel86a #automation #deduction
- The KLAUS Automated Deduction System (MES), pp. 703–704.
- CADE-1986-ThistlewaiteMM #automation #proving #theorem proving
- The KRIPKE Automated Theorem Proving System (PBT, MAM, RKM), pp. 705–706.
- CADE-1986-Wang86a
- SHD-Prover at University of Texas at Austin (TCW), pp. 707–708.

18 ×#proving

13 ×#theorem proving

10 ×#logic

8 ×#unification

6 ×#term rewriting

5 ×#automation

4 ×#deduction

4 ×#implementation

4 ×#induction

4 ×#named

13 ×#theorem proving

10 ×#logic

8 ×#unification

6 ×#term rewriting

5 ×#automation

4 ×#deduction

4 ×#implementation

4 ×#induction

4 ×#named