Proceedings of the 11th 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

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

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

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.

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.