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

- 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.

8 ×#proving

4 ×#algebra

4 ×#source code

4 ×#theorem proving

3 ×#using

2 ×#algorithm

2 ×#empirical

2 ×#how

2 ×#logic programming

2 ×#reasoning

4 ×#algebra

4 ×#source code

4 ×#theorem proving

3 ×#using

2 ×#algorithm

2 ×#empirical

2 ×#how

2 ×#logic programming

2 ×#reasoning