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

@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)

8 ×#proving
4 ×#algebra
4 ×#source code
4 ×#theorem proving
3 ×#using
2 ×#algorithm
2 ×#empirical
2 ×#how
2 ×#logic programming
2 ×#reasoning

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.