Ewing L. Lusk, Ross A. Overbeek
Proceedings of the Ninth International Conference on Automated Deduction
CADE, 1988.

@proceedings{CADE-1988,
	address       = "Argonne, Illinois, USA",
	editor        = "Ewing L. Lusk and Ross A. Overbeek",
	isbn          = "3-540-19343-X",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Ninth International Conference on Automated Deduction}",
	volume        = 310,
	year          = 1988,
}

Contents (73 items)

21 ×#proving
14 ×#named
14 ×#theorem proving
8 ×#automation
8 ×#logic
8 ×#prolog
8 ×#reasoning
5 ×#equation
5 ×#problem
5 ×#unification

CADE-1988-ZhangK #first-order #proving #theorem proving #using

First-Order Theorem Proving Using Conditional Rewrite Rules (HZ, DK), pp. 1–20.

CADE-1988-Wang #reasoning

Elements of Z-Module Reasoning (TCW), pp. 21–40.

CADE-1988-DonatW #higher-order #learning #using

Learning and Applying Generalised Solutions using Higher Order Resolution (MRD, LAW), pp. 41–60.

CADE-1988-FeltyM #higher-order #logic programming #programming language #proving #specification #theorem proving

Specifying Theorem Provers in a Higher-Order Logic Programming Language (APF, DM), pp. 61–80.

CADE-1988-Subrahmanian #logic programming #query

Query Processing in Quantitative Logic Programming (VSS), pp. 81–100.

CADE-1988-Basin #automation #reasoning

An Environment For Automated Reasoning About Partial Functions (DAB), pp. 101–110.

CADE-1988-Bundy #induction #proving #using

The Use of Explicit Plans to Guide Inductive Proofs (AB), pp. 111–120.

CADE-1988-DuchierM #development #interactive #named #proving

LOGICALC: An Environment for Interactive Proof Development (DD, DVM), pp. 121–130.

CADE-1988-HeiselRS #implementation #verification

Implementing Verification Strategies in the KIV-System (MH, WR, WS), pp. 131–140.

CADE-1988-Simon #natural language #proving

Checking Natural Language Proofs (DS), pp. 141–150.

CADE-1988-Bezem #consistency #rule-based

Consistency of Rule-based Expert System (MB), pp. 151–161.

CADE-1988-ZhangKK #equation #induction #specification

A Mechanizable Induction Principle for Equational Specifications (HZ, DK, MSK), pp. 162–181.

CADE-1988-GallierNPRS #canonical #equation #finite #polynomial #set #term rewriting

Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time (JHG, PN, DAP, SR, WS), pp. 182–196.

CADE-1988-McRobbieMT #automation #knowledge-based #logic #performance #proving #standard #theorem proving #towards

Towards Efficient “Knowledge-Based” Automated Theorem Proving for Non-Standard Logics (MAM, RKM, PBT), pp. 197–217.

CADE-1988-AabyN #logic

Propositional Temporal Interval Logic is PSPACE Complete (AAA, KTN), pp. 218–237.

CADE-1988-Howe

Computational Metatheory in Nuprl (DJH), pp. 238–257.

CADE-1988-Azzoune #prolog #type inference

Type Inference in Prolog (HA), pp. 258–277.

CADE-1988-MinkerR #logic programming #source code

Procedural Interpretation of Non-Horn Logic Programs (JM, AR), pp. 278–293.

CADE-1988-ChiH #horn clause #query #recursion

Recursive Query Answering with Non-Horn Clauses (SC, LJH), pp. 294–312.

CADE-1988-WakayamaP

Case Inference in Resolution-Based Languages (TW, THP), pp. 313–322.

CADE-1988-ButlerLO #automaton #compilation #performance #program transformation #prolog

Notes on Prolog Program Transformations, Prolog Style, and Efficient Compilation to The Warren Abstract Machine (RB, RL, RO), pp. 323–332.

CADE-1988-ButlerK #deduction #parallel #problem #prototype

Exploitation of Parallelism in Prototypical Deduction Problems (RB, NTK), pp. 333–343.

CADE-1988-Moser #graph

A Decision Procedure for Unquantified Formulas of Graph Theory (LEM), pp. 344–357.

CADE-1988-LincolnC #commutative #unification

Adventures in Associative-Commutative Unification (PL, JC), pp. 358–367.

CADE-1988-Buttner #algebra #finite #unification

Unification in Finite Algebras is Unitary (?) (WB), pp. 368–377.

CADE-1988-Schmidt-Schauss #equation #unification

Unification in a Combination of Arbitrary Disjoint Equational Theories (MSS), pp. 378–396.

CADE-1988-BlasiusS #equation #graph #reasoning #unification

Partial Unification for Graph Based Equational Reasoning (KHB, JHS), pp. 397–414.

CADE-1988-MantheyB #named #prolog #proving #theorem proving

SATCHMO: A Theorem Prover Implemented in Prolog (RM, FB), pp. 415–434.

CADE-1988-PotterP #term rewriting

Term Rewriting: Some Experimental Results (RCP, DAP), pp. 435–453.

CADE-1988-BrockCP #proving #reasoning

Analogical Reasoning and Proof Discovery (BB, SC, WP), pp. 454–468.

CADE-1988-Hines #knowledge-based #proving #theorem proving

Hyper-Chaining and Knowledge-Based Theorem Proving (LMH), pp. 469–486.

CADE-1988-CerroH #deduction #linear

Linear Modal Deductions (LFdC, AH), pp. 487–499.

CADE-1988-Ohlbach #calculus #logic

A Resolution Calculus for Modal Logics (HJO), pp. 500–516.

CADE-1988-Burckert #equation

Solving Disequations in Equational Theories (HJB), pp. 517–526.

CADE-1988-KounalisR #on the #problem #word

On Word Problems in Horn Theories (EK, MR), pp. 527–537.

CADE-1988-DershowitzOS #canonical #term rewriting

Canonical Conditional Rewrite Systems (ND, MO, GS), pp. 538–549.

CADE-1988-Jacquet #synthesis #type system

Program Synthesis by Completion with Dependent Subtypes (PJ), pp. 550–562.

CADE-1988-Kafl #linear #reasoning

Reasoning about Systems of Linear Inequalities (TK), pp. 563–572.

CADE-1988-Socher #algorithm #matrix

A Subsumption Algorithm Based on Characteristic Matrices (RS), pp. 573–581.

CADE-1988-Rabinov #strict

A Restriction of Factoring in Binary Resolution (AR), pp. 582–591.

CADE-1988-BesnardS #automation #logic #reasoning

Supposition-Based Logic for Automated Nonmontonic Reasoning (PB, PS), pp. 592–601.

CADE-1988-Walther #algorithm #automation #bound #proving #termination

Argument-Bounded Algorithms as a Basis for Automated Termination Proofs (CW), pp. 602–621.

CADE-1988-MarcusR #automation #implementation #proving

Two Automated Methods in Implementation Proofs (LM, TR), pp. 622–642.

CADE-1988-FranzenH #approach #unification

A New Approach to Universal Unification and Its Application to AC-Unification (MF, LJH), pp. 643–657.

CADE-1988-MurrayR #implementation

An Implementation of a Dissolution-Based System Employing Theory Links (NVM, ER), pp. 658–674.

CADE-1988-Niemela #logic

Decision Procedure for Autoepistemic Logic (IN), pp. 675–684.

CADE-1988-MalkinM #generative #logic #matrix #testing

Logical Matrix Generation and Testing (PKM, EPM), pp. 685–693.

CADE-1988-VermaR #bound #parallel

Optimal Time Bounds for Parallel Term Matching (RMV, IVR), pp. 694–703.

CADE-1988-McCune #challenge #problem #similarity

Challenge Equality Problems in Lattice Theory (WM), pp. 704–709.

CADE-1988-Pfenning #axiom #calculus

Single Axioms in the Implicational Propositional Calculus (FP), pp. 710–713.

CADE-1988-WosM #automation #challenge #combinator #logic #problem #similarity #source code

Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs (LW, WM), pp. 714–729.

CADE-1988-Stevens #challenge #problem #proving #theorem proving

Challenge Problems from Nonassociative Rings for Theorem Provers (RLS), pp. 730–734.

CADE-1988-Kaufmann #interactive #proving #theorem proving

An Interactive Enhancement to the Boyer-Moore Theorem Prover (MK), pp. 735–736.

CADE-1988-Plaisted #proving #theorem proving

A Goal Directed Theorem Prover (DAP), p. 737.

CADE-1988-PaseK #summary

m-NEVER System Summary (BP, SK), pp. 738–739.

CADE-1988-Griffin #interactive #named

EFS — An Interactive Environment for Formal Systems (TG), pp. 740–741.

CADE-1988-McAllester #information management #named #representation

Ontic: A Knowledge Representation System for Mathematics (DAM), pp. 742–743.

CADE-1988-TourCC #tool support

Some Tools for an Inference Laboratory (ATINF) (TBdlT, RC, GC), pp. 744–745.

CADE-1988-SubrahmanianU #approximate #consistency #named #reasoning

QUANTLOG: A System for Approximate Reasoning in Inconsistent Formal Systems (VSS, ZDU), pp. 746–747.

CADE-1988-GarlandG #named #proving

LP: The Larch Prover (SJG, JVG), pp. 748–749.

CADE-1988-Stickel #automation #deduction

The KLAUS Automated Deduction System (MES), pp. 750–751.

CADE-1988-Stickel88a #prolog #proving #theorem proving

A Prolog Technology Theorem Prover (MES), pp. 752–753.

CADE-1988-FeltyGHMNS #logic programming #named #programming language #prolog #λ-calculus

Lambda-Prolog: An Extended Logic Programming Language (APF, ELG, JH, DM, GN, AS), pp. 754–755.

CADE-1988-BrownP #logic #named #proving #theorem proving

SYMEVAL: A Theorem Prover Based on the Experimental Logic (FMB, SSP), pp. 756–757.

CADE-1988-BrownPP #automation #named #reasoning

ZPLAN: An Automatic Reasoning System for Situations (FMB, SSP, JP), pp. 758–759.

CADE-1988-AndrewsINP #proving #theorem proving

The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.

CADE-1988-BieberCH #named #prolog

MOLOG: a Modal PROLOG (PB, LFdC, AH), pp. 762–763.

CADE-1988-AllenBCM #horn clause #named #parallel #proving #theorem proving

PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.

CADE-1988-SmithL #implementation #prolog

An nH-Prolog Implementation (BTS, DWL), pp. 766–767.

CADE-1988-KapurZ #named

RRL: A Rewrite Rule Laboratory (DK, HZ), pp. 768–769.

CADE-1988-CyrlukHK #algebra #geometry #named #proving #theorem proving

GEOMETER: A Theorem Prover for Algebraic Geometry (DC, RMH, DK), pp. 770–771.

CADE-1988-Paulson #named #proving #theorem proving

Isabelle: The Next Seven Hundred Theorem Provers (LCP), pp. 772–773.

CADE-1988-DincbasHSAH #constraints #prolog

The CHIP System: Constraint Handling In Prolog (MD, PVH, HS, AA, AH), pp. 774–775.