5th Conference on Automated Deduction: Les Arcs, France, July 8-11, 1980: v. 87 (Lecture Notes in Computer Science)

R. Kowalski, W. Bibel

ISBN 10: 3540100091 / ISBN 13: 9783540100096

Published by Springer 2008-06-13, 2008

About this Item

Seller Inventory # 6666-IUK-9783540100096

Bibliographic Details

• Title: 5th Conference on Automated Deduction: Les Arcs, France, July 8-11, 1980: v. 87 (Lecture Notes in Computer Science)
• Publisher: Springer 2008-06-13
• Publication Date: 2008
• Language: English
• ISBN 10: 3540100091
• ISBN 13: 9783540100096
• Binding: Paperback
• Condition: New

About this title

Synopsis

Using meta-theoretic reasoning to do algebra.- Generating contours of 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 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.- A refinement of paramodulation.- The AFFIRM theorem Proof forests and management of large proofs.- Data structures and control architecture for implementation of theorem-proving programs.- A note on 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 Choose your term algebra carefully.- How to prove algebraic inductive hypotheses without induction.- A complete, nonredundant algorithm for reversed skolemization.