Proceedings of the Fifth 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

Wolfgang Bibel, Robert A. Kowalski
Proceedings of the Fifth International Conference on Automated Deduction
CADE, 1980.

TEST
DBLP
Scholar
Full names Links ISxN
@proceedings{CADE-1980,
	address       = "Les Arcs, France",
	editor        = "Wolfgang Bibel and Robert A. Kowalski",
	isbn          = "3-540-10009-1",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Fifth International Conference on Automated Deduction}",
	volume        = 87,
	year          = 1980,
}

Contents (28 items)

CADE-1980-AielloW #algebra #reasoning #using
Using Meta-Theoretic Reasoning to do Algebra (LCA, RWW), pp. 1–13.
CADE-1980-BelovariC #generative #integration #prolog
Generating Contours of Integration: An Application of Prolog in Symbolic Computing (GB, JAC), pp. 14–23.
CADE-1980-BundyW #algebra #multi #using
Using Meta-Level Inference for Selective Application of Multiple Rewrite Rules in Algebraic Manipulation (AB, BW), pp. 24–38.
CADE-1980-Goad #proving
Proofs as Description of Computation (CG), pp. 39–52.
CADE-1980-GuihoG #synthesis
Program Synthesis from Incomplete Specifiactions (GDG, CG), pp. 53–62.
CADE-1980-Kott #proving #recursion #source code
A System for Proving Equivalences of Recursive Programs (LK), pp. 63–69.
CADE-1980-BledsoeH #proving
Variable Elimination and Chaining in a Resolution-based Prover for Inequalities (WWB, LMH), pp. 70–87.
CADE-1980-FerroOS #set
Decision Procedures for Some Fragments of Set Theory (AF, EGO, JTS), pp. 88–96.
CADE-1980-LovelandS
Simplifying Interpreted Formulas (DWL, RES), pp. 97–109.
CADE-1980-Furtek #constraints #distributed #formal method #realtime #specification #using #verification
Specification and Verification of Real-Time, Distributed Systems Using the Theory of Constraints (FCF), pp. 110–125.
CADE-1980-Friedman #reasoning
Reasoning by Plausible Inference (LF), pp. 126–142.
CADE-1980-Thompson #logic
Logical Support in a Time-Varying Model (AMT), pp. 143–153.
CADE-1980-Gloess #correctness #empirical #parsing #proving #theorem proving
An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions (PYG), pp. 154–169.
CADE-1980-Leszczylowski #empirical
An Experiment with “Edinburgh LCF” (JL), pp. 170–181.
CADE-1980-Nederpelt #approach #proving #theorem proving #λ-calculus
An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus (RN), pp. 182–194.
CADE-1980-GloessL #algorithm
Adding Dynamic Paramodulation to Rewrite Algorithms (PYG, JPHL), pp. 195–207.
CADE-1980-WosOH #named #refinement
Hyperparamodulation: A Refinement of Paramodulation (LW, RAO, LJH), pp. 208–219.
CADE-1980-EricksonM #proving #scalability #theorem proving
The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs (RWE, DRM), pp. 220–231.
CADE-1980-OverbeekL #architecture #data type #implementation #source code
Data Structures and Control Architectures for Implementation of Theorem-Proving Programs (RAO, ELL), pp. 232–249.
CADE-1980-Noll #how
A Note on Resolution: How to Get Rid of Factoring without Loosing Completeness (HN), pp. 250–263.
CADE-1980-Plaisted #abstraction #proving #theorem proving
Abstraction Mappings in Mechanical Theorem Proving (DAP), pp. 264–280.
CADE-1980-Andrews #deduction #proving
Transforming Matings into Natural Deduction Proofs (PBA), pp. 281–292.
CADE-1980-Bruynooghe #analysis #behaviour #dependence #logic programming #source code
Analysis of Dependencies to Improve the Behaviour of Logic Programs (MB), pp. 293–305.
CADE-1980-PereiraP #backtracking #logic programming #source code
Selective Backtracking for Logic Programs (LMP, AP), pp. 306–317.
CADE-1980-Hullot #canonical #unification
Canonical Forms and Unification (JMH), pp. 318–334.
CADE-1980-Jeanrond #algebra #term rewriting #termination
Deciding Unique Termination of Permutative Rewriting Systems: Choose Your Term Algebra Carefully (HJJ), pp. 335–355.
CADE-1980-Guguen #algebra #how #induction
How to Prove Algebraic Inductive Hypotheses Without Induction (JAG), pp. 356–373.
CADE-1980-CoxP #algorithm
A Complete, Nonredundant Algorithm for Reversed Skolemization (PTC, TP), pp. 374–385.

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.