Proceedings of the Eighth International Conference on Automated Deduction
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

Jörg H. Siekmann
Proceedings of the Eighth International Conference on Automated Deduction
CADE, 1986.

TEST
DBLP
Scholar
Full names Links ISxN
@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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.