Format:
Online-Ressource (VII, 385 S.)
Edition:
Online-Ausg. Berlin [u.a.] Springer 2006 Springer lecture notes archive
ISBN:
9783540381402
Series Statement:
Lecture notes in computer science 87
Content:
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.
Note:
Literaturangaben
Additional Edition:
ISBN 3540100091
Additional Edition:
ISBN 0387100091
Additional Edition:
ISBN 9783540100096
Additional Edition:
Erscheint auch als Druck-Ausgabe Conference on Automated Deduction (5 : 1980 : Les Arcs) 5th Conference on Automated Deduction Berlin [u.a.] : Springer, 1980 ISBN 3540100091
Additional Edition:
ISBN 0387100091
Language:
English
Keywords:
Konferenzschrift
DOI:
10.1007/3-540-10009-1
URL:
Volltext
(lizenzpflichtig)
URL:
Volltext
(lizenzpflichtig)
URL:
Volltext
(lizenzpflichtig)
Author information:
Bibel, Wolfgang 1938-
