BibSLEIGH — Proceedings of the Eighth International Conference on Automated Deduction

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

TEST

@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.

Jörg H. SiekmannProceedings of the Eighth International Conference on Automated DeductionCADE, 1986.

Contents (72 items)

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