5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980 [electronic resource] /

Using meta-theoretic reasoning to do algebra -- Generating contours of integration: An application of PROLOG in symbolic computing -- Using meta-level inference for selective application of multiple rewrite rules in algebraic manipulation -- Proofs as descriptions of computation -- Program synthesis from incomplete specifications -- A system for proving equivalences of recursive programs -- Variable elimination and chaining in a resolution-based prover for inequalities -- Decision procedures for some fragments of set theory -- Simplifying interpreted formulas -- Specification and verification of real-time, distributed systems using the theory of constraints -- Reasoning by plausible inference -- Logical support in a time-varying model -- An experiment with the Boyer-Moore theorem prover: A proof of the correctness of a simple parser of expressions -- An experiment with "Edinburgh LCF" -- An approach to theorem proving on the basis of a typed lambda-calculus -- Adding dynamic paramodulation to rewrite algorithms -- Hyperparamodulation: A refinement of paramodulation -- The AFFIRM theorem prover: Proof forests and management of large proofs -- Data structures and control architecture for implementation of theorem-proving programs -- A note on resolution: How to get rid of factoring without loosing completeness -- Abstraction mappings in mechanical theorem proving -- Transforming matings into natural deduction proofs -- Analysis of dependencies to improve the behaviour of logic programs -- Selective backtracking for logic programs -- Canonical forms and unification -- Deciding unique termination of permutative rewriting systems: Choose your term algebra carefully -- How to prove algebraic inductive hypotheses without induction -- A complete, nonredundant algorithm for reversed skolemization.

Bibliographic Details

Main Authors:	Bibel, Wolfgang. editor., Kowalski, Robert. editor., SpringerLink (Online service)
Format:	Texto biblioteca
Language:	eng
Published:	Berlin, Heidelberg : Springer Berlin Heidelberg, 1980
Subjects:	Mathematics., Mathematical logic., Mathematical Logic and Foundations., Mathematical Logic and Formal Languages.,
Online Access:	http://dx.doi.org/10.1007/3-540-10009-1
Tags:	Add Tag No Tags, Be the first to tag this record!