5. CADE 1980: Les Arcs, France

@proceedings{DBLP:conf/cade/1980,
  editor    = {Wolfgang Bibel and
               Robert A. Kowalski},
  title     = {5th Conference on Automated Deduction, Les Arcs, France, July
               8-11, 1980, Proceedings},
  booktitle = {CADE},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {87},
  year      = {1980},
  isbn      = {3-540-10009-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Tuesday Morning

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

Tuesday Afternoon

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

Wednesday Morning

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

Thursday Morning

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

Thursday Afternoon

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

Friday Morning

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

Friday Afternoon

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