Deepak Kapur
Proceedings of the 11th International Conference on Automated Deduction
CADE, 1992.

@proceedings{CADE-1992,
	address       = "Saratoga Springs, New York, USA",
	editor        = "Deepak Kapur",
	isbn          = "3-540-55602-8",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 11th International Conference on Automated Deduction}",
	volume        = 607,
	year          = 1992,
}

Contents (74 items)

26 ×#proving
15 ×#theorem proving
10 ×#automation
10 ×#logic
10 ×#named
6 ×#unification
5 ×#deduction
4 ×#parallel
3 ×#semantics
3 ×#set

CADE-1992-Wos #automation #logic #reasoning

The Impossibility of the Automation of Logical Reasoning (LW), pp. 1–3.

CADE-1992-Ammon #analysis #automation #logic #proving

Automatic Proofs in Mathematical Logic and Analysis (KA), pp. 4–19.

CADE-1992-ChouG #geometry #proving

Proving Geometry Statements of Constructive Type (SCC, XSG), pp. 20–34.

CADE-1992-Hines

The Central Variable Strategy of Str+ve (LMH), pp. 35–49.

CADE-1992-BaaderS #equation #unification

Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures (FB, KUS), pp. 50–65.

CADE-1992-NipkowQ #reduction #type system #unification #λ-calculus

Reduction and Unification in Lambda Calculi with Subtypes (TN, ZQ), pp. 66–78.

CADE-1992-DoughertyJ #approach #combinator #higher-order #logic

A Combinatory Logic Approach to Higher-order E-unification (DJD, PJ), pp. 79–93.

CADE-1992-BibelHW #unification

Cycle Unification (WB, SH, JW), pp. 94–108.

CADE-1992-YelickG #parallel #term rewriting

A Parallel Completion Procedure for Term Rewriting Systems (KAY, SJG), pp. 109–123.

CADE-1992-McAllester

Grammar Rewriting (DAM), pp. 124–138.

CADE-1992-CichonL #algorithm #complexity #polynomial

Polynomial Interpretations and the Complexity of Algorithms (AC, PL), pp. 139–147.

CADE-1992-FegarasSS #combinator #traversal

Uniform Traversal Combinators: Definition, Use and Properties (LF, TS, DWS), pp. 148–162.

CADE-1992-Uribe #constraints #set #unification #using

Sorted Unification Using Set Constraints (TEU), pp. 163–177.

CADE-1992-FrischC #unification

An Abstract View of Sorted Unification (AMF, AGC), pp. 178–192.

CADE-1992-Boudet #algebra #order #unification

Unification in Order-Sorted Algebras with Overloading (AB), pp. 193–207.

CADE-1992-Smullyan

Puzzles and Paradoxes (RMS), p. 208.

CADE-1992-McCuneW #automation #deduction

Experiments in Automated Deduction with Condensed Detachment (WM, LW), pp. 209–223.

CADE-1992-AstrachanS #proving #theorem proving

Caching and Lemmaizing in Model Elimination Theorem Provers (OLA, MES), pp. 224–238.

CADE-1992-DigricoliK #challenge #problem

LIM+ Challenge Problems by RUE Hyper-Resolution (VJD, EK), pp. 239–252.

CADE-1992-Jackson #incremental

Computing Prime Implicates Incrementally (PJ), pp. 253–267.

CADE-1992-Sutcliffe #analysis #set

Linear-Input Subset Analysis (GS), pp. 268–280.

CADE-1992-BenhamouS #calculus #symmetry

Theoretical Study of Symmetries in Propositional Calculus and Applications (BB, LS), pp. 281–294.

CADE-1992-BasinW #difference

Difference Matching (DAB, TW), pp. 295–309.

CADE-1992-HeskethBS #reasoning #recursion #source code #synthesis #using

Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs (JH, AB, AS), pp. 310–324.

CADE-1992-WalshNB #proving #theorem proving #using

The Use of Proof Plans to Sum Series (TW, AN, AB), pp. 325–339.

CADE-1992-Protzen

Disproving Conjectures (MP), pp. 340–354.

CADE-1992-Bauer #logic #multi

An Interval-based Temporal Logic in a Multivalued Setting (MB), pp. 355–369.

CADE-1992-Fisher #first-order #normalisation

A Normal Form for First-Order Temporal Formulae (MF), pp. 370–384.

CADE-1992-CaferraD #logic #proving #semantics

Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic (RC, SD), pp. 385–399.

CADE-1992-InoueKH #generative #proving #theorem proving

Embedding Negation as Failure into a Model Generation Theorem Prover (KI, MK, RH), pp. 400–415.

CADE-1992-BoyerY #automation #correctness #proving #source code

Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor (RSB, YY), pp. 416–430.

CADE-1992-ZhangH #induction #proving #set #theorem

Proving the Chinese Remainder Theorem by the Cover Set Induction (HZ, XH), pp. 431–445.

CADE-1992-Madden #automation #optimisation #proving

Automatic Program Optimization Through Proof Transformation (PM), pp. 446–460.

CADE-1992-BachmairGLS

Basic Paramodulation and Superposition (LB, HG, CL, WS), pp. 462–476.

CADE-1992-NieuwenhuisR #proving #theorem proving

Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.

CADE-1992-MannaW

The Special-Relation Rules are Incomplete (ZM, RJW), pp. 492–506.

CADE-1992-BeckertH #semantics #similarity

An Improved Method for Adding Equality to Free Variable Semantic Tableaux (BB, RH), pp. 507–521.

CADE-1992-Shankar #calculus #proving

Proof Search in the Intuitionistic Sequent Calculus (NS), pp. 522–536.

CADE-1992-PfenningR #deduction #implementation

Implementing the Meta-Theory of Deductive Systems (FP, ER), pp. 537–551.

CADE-1992-Chen #empirical #knowledge-based #proving #theorem proving

Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic (WZC), pp. 552–566.

CADE-1992-FarmerGT

Little Theories (WMF, JDG, FJT), pp. 567–581.

CADE-1992-Christian #termination

Some Termination Criteria for Narrowing and E-Narrowing (JC), pp. 582–588.

CADE-1992-DershowitzMS #convergence #decidability

Decidable Matching for Convergent Systems (ND, SM, GS), pp. 589–602.

CADE-1992-Kesner #order #orthogonal #term rewriting

Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors (DK), pp. 603–617.

CADE-1992-SekarR #equation #evaluation #framework #lazy evaluation #parallel #programming

Programming with Equations: A Framework for Lazy Parallel Evaluation (RCS, IVR), pp. 618–632.

CADE-1992-Cohn #logic

A Many Sorted Logic with Possibly Empty Sorts (AGC), pp. 633–647.

CADE-1992-Voronkov #logic #proving #standard #theorem proving

Theorem Proving in Non-Standard Logics Based on the Inverse Method (AV), pp. 648–662.

CADE-1992-VershininR #logic #nondeterminism

One More Logic with Uncertainty and Resolution Principle for it (KV, IR), pp. 663–667.

CADE-1992-Dafa #automation #deduction #proving #theorem proving

A Natural Deduction Automated Theorem Proving System (LD), pp. 668–672.

CADE-1992-NipkowP

Isabelle-91 (TN, LCP), pp. 673–676.

CADE-1992-Sutcliffe92a #deduction #linear #semantics

The Semantically Guided Linear Deduction System (GS), pp. 677–680.

CADE-1992-Ammon92a

The SHUNYATA System (KA), pp. 681–685.

CADE-1992-Chou #geometry #proving #theorem proving

A Geometry Theorem Prover for Macintoshes (SCC), pp. 686–690.

CADE-1992-HuaZ #induction #named

FRI: Failure-Resistant Induction in RRL (XH, HZ), pp. 691–695.

CADE-1992-Zhang #named #performance

Herky: High Performance Rewriting in RRL (HZ), pp. 696–700.

CADE-1992-FarmerGT92a #named

IMPS: System Description (WMF, JDG, FJT), pp. 701–705.

CADE-1992-AlexanderP #proving #similarity #theorem

Proving Equality Theorems with Hyper-Linking (GDA, DAP), pp. 706–710.

CADE-1992-ChirimarGI #interface #named #performance #proving #visual notation

Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker (JC, CAG, MVI), pp. 711–715.

CADE-1992-Baker-PlummerBM #automation #deduction

&: Automated Natural Deduction (DBP, SCB, ASM), pp. 716–720.

CADE-1992-UribeFM #automation #framework #overview #proving

An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems (TEU, AMF, MKM), pp. 721–725.

CADE-1992-Baker-PlummerR #proving #theorem proving

The GAZER Theorem Prover (DBP, AR), pp. 726–730.

CADE-1992-LuskMS #named #parallel #proving #theorem proving

ROO: A Parallel Theorem Prover (ELL, WM, JKS), pp. 731–734.

CADE-1992-WangG #automation #named #verification

RVF: An Automated Formal Verification System (TCW, AG), pp. 735–739.

CADE-1992-Schumann #logic #named #proving #theorem proving

KPROP — An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (JS), pp. 740–742.

CADE-1992-Blackburn

A Report in ICL HOL (KB), pp. 743–747.

CADE-1992-OwreRS #named #prototype #verification

PVS: A Prototype Verification System (SO, JMR, NS), pp. 748–752.

CADE-1992-Reif

The KIV System: Systematic Construction of Verified Software (WR), pp. 753–757.

CADE-1992-BeckertGHK #logic #multi #proving #theorem proving

The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics (BB, SG, RH, WK), pp. 758–760.

CADE-1992-ClarkeZ #named #proving #theorem proving

Analytica — A Theorem Prover in Mathematica (EMC, XZ), pp. 761–765.

CADE-1992-SchneiderKK #proving

The FAUST — Prover (KS, RK, TK), pp. 766–770.

CADE-1992-CraigenKMPS

Eves System Description (DC, SK, IM, BP, MS), pp. 771–775.

CADE-1992-HasegawaKF #generative #lazy evaluation #named #parallel #proving #theorem proving

MGTP: A Parallel Theorem Prover Based on Lazy Model Generation (RH, MK, HF), pp. 776–780.

CADE-1992-LuskW #benchmark #metric #problem #similarity

Benchmark Problems in Which Equality Plays the Major Role (ELL, LW), pp. 781–785.

CADE-1992-RandellCC #automation #challenge #proving #theorem proving

Computing Transivity Tables: A Challenge For Automated Theorem Provers (DAR, AGC, ZC), pp. 786–790.