Alan Bundy
Proceedings of the 12th International Conference on Automated Deduction
CADE, 1994.

@proceedings{CADE-1994,
	address       = "Nancy, France",
	editor        = "Alan Bundy",
	isbn          = "3-540-58156-1",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 12th International Conference on Automated Deduction}",
	volume        = 814,
	year          = 1994,
}

Contents (72 items)

22 ×#proving
13 ×#named
8 ×#induction
8 ×#theorem proving
6 ×#automation
5 ×#deduction
5 ×#order
5 ×#problem
4 ×#logic
4 ×#on the

CADE-1994-Slaney #automation #finite #reasoning

The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure (JKS), pp. 1–13.

CADE-1994-Walsh

A Divergence Critic (TW), pp. 14–28.

CADE-1994-Hutter #induction #order #proving #synthesis

Synthesis of Induction Orderings for Existence Proofs (DH), pp. 29–41.

CADE-1994-Protzen #generative #induction #lazy evaluation

Lazy Generation of Induction Hypotheses (MP), pp. 42–56.

CADE-1994-Plaisted #performance #proving #theorem proving

The Search Efficiency of Theorem Proving Strategies (DAP), pp. 57–71.

CADE-1994-BourelyCP #automation #modelling

A Method for Building Models Automatically. Experiments with an Extension of OTTER (CB, RC, NP), pp. 72–86.

CADE-1994-BaumgartnerF

Model Elimination Without Contrapositives (PB, UF), pp. 87–101.

CADE-1994-BronsardRH #induction #order #using

Induction using Term Orderings (FB, USR, RWH), pp. 102–117.

CADE-1994-ChazarainK #induction #proving

Mechanizable Inductive Proofs for a Class of Forall Exists Formulas (JC, EK), pp. 118–132.

CADE-1994-Lysne #consistency #on the #proving

On the Connection between Narrowing and Proof by Consistency (OL), pp. 133–147.

CADE-1994-Paulson #approach #implementation #induction

A Fixedpoint Approach to Implementing (Co)Inductive Definitions (LCP), pp. 148–161.

CADE-1994-WirthG #equation #induction #on the

On Notions of Inductive Validity for First-Oder Equational Clauses (CPW, BG), pp. 162–176.

CADE-1994-Baker #automation #deduction

A New Application for Explanation-Based Generalisation within Automated Deduction (SB), pp. 177–191.

CADE-1994-ChuP #first-order #proving #semantics #theorem proving #using

Semantically Guided First-Order Theorem Proving using Hyper-Linking (HC, DAP), pp. 192–206.

CADE-1994-WaalG #logic programming #program analysis #program transformation #proving #theorem proving

The Applicability of Logic Program Analysis and Transformation to Theorem Proving (DAdW, JPG), pp. 207–221.

CADE-1994-Bruning #detection

Detecting Non-Provable Goals (SB), pp. 222–236.

CADE-1994-Anonymous

The QED Manifesto, pp. 238–251.

CADE-1994-SutcliffeSY #library #problem

The TPTP Problem Library (GS, CBS, TY), pp. 252–266.

CADE-1994-DomenjoudKR #equation

Combination Techniques for Non-Disjoint Equational Theories (ED, FK, CR), pp. 267–281.

CADE-1994-Salzer #unification

Primal Grammars and Unification Modulo a Binary Clause (GS), pp. 282–295.

CADE-1994-Iwanuma #normalisation #parallel #query

Conservative Query Normalization on Parallel Circumscription (KI), pp. 296–310.

CADE-1994-FribourgP #bottom-up #constraints #datalog #evaluation #source code

Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints (LF, MVP), pp. 311–325.

CADE-1994-RoyerQ #on the #query

On Intuitionistic Query Answering in Description Bases (VR, JQ), pp. 326–340.

CADE-1994-StickelWLPU #composition #deduction #library

Deductive Composition of Astronomical Software from Subroutine Libraries (MES, RJW, MRL, TP, IU), pp. 341–355.

CADE-1994-FarmerGNT #proving

Proof Script Pragmatics in IMPS (WMF, JDG, MEN, FJT), pp. 356–370.

CADE-1994-KerberK #logic

A Mechanization of Strong Kleene Logic for Partial Functions (MK, MK), pp. 371–385.

CADE-1994-Wang #algebra #geometry #proving

Algebraic Factoring and Geometry Proving (DW), pp. 386–400.

CADE-1994-McPheeCG #geometry #proving #theorem #using

Mechanically Proving Geometry Theorems Using a Combination of Wu’s Method and Collins’ Method (NFM, SCC, XSG), pp. 401–415.

CADE-1994-Hines #integer

Str+ve and Integers (LMH), pp. 416–430.

CADE-1994-Platek #proving #question #what

What is a Proof? (RP), p. 431.

CADE-1994-Martin #geometry #invariant #termination

Termination, Geometry and Invariants (UM), pp. 432–434.

CADE-1994-BachmairG #order

Ordered Chaining for Total Orderings (LB, HG), pp. 435–450.

CADE-1994-MiddeldorpZ #revisited #termination

Simple Termination Revisited (AM, HZ), pp. 451–465.

CADE-1994-BasinW #order #termination

Termination Orderings for Rippling (DAB, TW), pp. 466–483.

CADE-1994-SturgillS #first-order #logic #novel #parallel

A Novel Asynchronous Parallelism Scheme for First-Order Logic (DBS, AMS), pp. 484–498.

CADE-1994-Goubault #proving

Proving with BDDs and Control of Information (JG), pp. 499–513.

CADE-1994-Graf

Extended Path-Indexing (PG), pp. 514–528.

CADE-1994-Constable

Exporting and Refecting Abstract Metamathematics (RLC), p. 529.

CADE-1994-Vigneron #commutative #constraints #deduction

Associative-Commutative Deduction with Constraints (LV), pp. 530–544.

CADE-1994-NieuwenhuisR #constraints

AC-Superposition with Constraints: No AC-Unifiers Needed (RN, AR), pp. 545–559.

CADE-1994-HermannK #complexity #equation #problem

The Complexity of Counting Problems in Equational Matching (MH, PGK), pp. 560–574.

CADE-1994-Anderson #optimisation #proving #representation

Representing Proof Transformations for Program Optimizations (PA), pp. 575–589.

CADE-1994-Jackson #algebra #type system

Exploring Abstract Algebra in Constructive Type Theory (PJ), pp. 590–604.

CADE-1994-FeltyH #proving #theorem proving

Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables (APF, DJH), pp. 605–619.

CADE-1994-JohannK #constant #order #unification #λ-calculus

Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading (PJ, MK), pp. 620–634.

CADE-1994-Prehofer #decidability #higher-order #problem #unification

Decidable Higher-Order Unification Problems (CP), pp. 635–649.

CADE-1994-MullerW #composition #higher-order #theory and practice

Theory and Practice of Minimal Modular Higher-Order E-Unification (OM, FW), pp. 650–664.

CADE-1994-Socher-Ambrosius

A Refined Version of General E-Unification (RSA), pp. 665–677.

CADE-1994-Beckert

A Completion-Based Method for Mixed Universal and Rigid E-Unification (BB), pp. 678–692.

CADE-1994-Bundgen #how #on the

On Pot, Pans and Pudding or How to Discover Generalised Critical Pairs (RB), pp. 693–707.

CADE-1994-KlingenbeckH #semantics #strict

Semantic Tableaux with Ordering Restrictions (SK, RH), pp. 708–722.

CADE-1994-Massacci #logic

Strongly Analytic Tableaux for Normal Modal Logics (FM), pp. 723–737.

CADE-1994-Huang #proving #re-engineering

Reconstruction Proofs at the Assertion Level (XH), pp. 738–752.

CADE-1994-Zhang #finite #generative #modelling #problem

Problems on the Generation of Finite Models (JZ0), pp. 753–757.

CADE-1994-ClarkeZ #problem #proving #symbolic computation #theorem proving

Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (EMC, XZ), pp. 758–763.

CADE-1994-SlaneyLM #named #semantics

SCOTT: Semantically Constrained Otter System Description (JKS, ELL, WM), pp. 764–768.

CADE-1994-BaumgartnerF94a #interface #named #proving

PROTEIN: A PROver with a Theory Extension INterface (PB, UF), pp. 769–773.

CADE-1994-Schumann #bottom-up #named #preprocessor #proving #theorem proving #top-down

DELTA — A Bottom-up Preprocessor for Top-Down Theorem Provers — System Abstract (JS), pp. 774–777.

CADE-1994-GollerLMS

SETHEO V3.2: Recent Developments — System Abstract (CG, RL, KM, JS), pp. 778–782.

CADE-1994-BibelBER

KoMeT (WB, SB, UE, TR), pp. 783–787.

CADE-1994-HuangKKMNRS #development #named #proving

Omega-MKRP: A Proof Development Environment (XH, MK, MK, EM, DN, JR, JHS), pp. 788–792.

CADE-1994-BeckertP #agile #named #proving #theorem proving

leanTAP: Lean Tableau-Based Theorem Proving (BB, JP), pp. 793–797.

CADE-1994-Slaney94a #finite #named

FINDER: Finite Domain Enumerator — System Description (JKS), pp. 798–801.

CADE-1994-Portoraro #automation #named #proving

Symlog: Automated Advice in Fitch-style Proof Construction (FDP), pp. 802–806.

CADE-1994-HuangKKMNRS94a #automation #deduction #named #tool support

KEIM: A Toolkit for Automated Deduction (XH, MK, MK, EM, DN, JR, JHS), pp. 807–810.

CADE-1994-Pfenning #deduction #metalanguage #named

Elf: A Meta-Language for Deductive Systems (FP), pp. 811–815.

CADE-1994-OhtaniSM

EUODHILOS-II on Top of GNU Epoch (TO, HS, TM), pp. 816–820.

CADE-1994-Eriksson #calculus #editing #induction #interactive #named

Pi: an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions (LHE), pp. 821–825.

CADE-1994-RichardsKSW #logic #named

Mollusc: A General Proof-Development Shell for Sequent-Based Logics (BLR, IK, AS, GAW), pp. 826–830.

CADE-1994-WangG #automation #named #program analysis

KITP-93: An Automated Inference System for Program Analysis (TCW, AG), pp. 831–835.

CADE-1994-Bouhoula #induction #named #proving

SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs (AB), pp. 836–840.

CADE-1994-BonacinaM #distributed #proving #theorem proving

Distributed Theorem Proving by Peers (MPB, WM), pp. 841–845.