5. CADE 1980: Les Arcs, France

Wolfgang Bibel, Robert A. Kowalski (Eds.): 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings. Lecture Notes in Computer Science 87 Springer 1980, ISBN 3-540-10009-1

Tuesday Morning

Luigia Carlucci Aiello, Richard W. Weyhrauch:
Using Meta-Theoretic Reasoning to do Algebra. 1-13
Gábor Belovári, J. A. Campbell:
Generating Contours of Integration: An Application of Prolog in Symbolic Computing. 14-23
Alan Bundy, Bob Welham:
Using Meta-Level Inference for Selective Application of Multiple Rewrite Rules in Algebraic Manipulation. 24-38

Chris Goad:
Proofs as Description of Computation. 39-52
Gérard D. Guiho, Christian Gresse:
Program Synthesis from Incomplete Specifiactions. 53-62
Laurent Kott:
A System for Proving Equivalences of Recursive Programs. 63-69

W. W. Bledsoe, Larry M. Hines:
Variable Elimination and Chaining in a Resolution-based Prover for Inequalities. 70-87
Alfredo Ferro, Eugenio G. Omodeo, Jacob T. Schwartz:
Decision Procedures for Some Fragments of Set Theory. 88-96
Donald W. Loveland, Robert E. Shostak:
Simplifying Interpreted Formulas. 97-109
Frederick C. Furtek:
Specification and Verification of Real-Time, Distributed Systems Using the Theory of Constraints. 110-125
Leonard Friedman:
Reasoning by Plausible Inference. 126-142
Alan M. Thompson:
Logical Support in a Time-Varying Model. 143-153

Paul Y. Gloess:
An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions. 154-169
Jacek Leszczylowski:
An Experiment with "Edinburgh LCF". 170-181
Rob Nederpelt:
An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus. 182-194
Paul Y. Gloess, Jean-Pierre H. Laurent:
Adding Dynamic Paramodulation to Rewrite Algorithms. 195-207
Larry Wos, Ross A. Overbeek, Lawrence J. Henschen:
Hyperparamodulation: A Refinement of Paramodulation. 208-219

Roddy W. Erickson, David R. Musser:
The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs. 220-231
Ross A. Overbeek, Ewing L. Lusk:
Data Structures and Control Architectures for Implementation of Theorem-Proving Programs. 232-249

Helga Noll:
A Note on Resolution: How to Get Rid of Factoring without Loosing Completeness. 250-263
David A. Plaisted:
Abstraction Mappings in Mechanical Theorem Proving. 264-280
Peter B. Andrews:
Transforming Matings into Natural Deduction Proofs. 281-292
Maurice Bruynooghe:
Analysis of Dependencies to Improve the Behaviour of Logic Programs. 293-305
Luís Moniz Pereira, António Porto:
Selective Bachtracking for Logic Programs. 306-317

Jean-Marie Hullot:
Canonical Forms and Unification. 318-334
Hans-Josef Jeanrond:
Deciding Unique Termination of Permutative Rewriting Systems: Choose Your Term Algebra Carefully. 335-355
Joseph A. Goguen:
How to Prove Algebraic Inductive Hypotheses Without Induction. 356-373
Philip T. Cox, Tomasz Pietrzykowski:
A Complete, Nonredundant Algorithm for Reversed Skolemization. 374-385