default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID5th CADE 1980: Les Arcs, France
- Wolfgang Bibel, Robert A. Kowalski:
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, John 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
Tuesday Afternoon
- 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
Wednesday Morning
- 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
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 - 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
Thursday Afternoon
- 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
Friday Morning
- 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 Backtracking for Logic Programs. 306-317
Friday Afternoon
- 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2026-01-30 22:58 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
