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

Kowalski, R.; Bibel, W.

 
9783540100096: 5th Conference on Automated Deduction: Les Arcs, France, July 8-11, 1980 (Lecture Notes in Computer Science, 87, Band 87)
Softcover
ISBN 10: 3540100091 ISBN 13: 9783540100096
Verlag: Springer, 2008

Inhaltsangabe

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.

Die Inhaltsangabe kann sich auf eine andere Ausgabe dieses Titels beziehen.

Verlag
Springer
Erscheinungsdatum
2008
Sprache
Englisch
ISBN 10 
3540100091
ISBN 13 
9783540100096
Einband
Taschenbuch
Anzahl der Seiten
408
Kontakt zum Hersteller
ProductSafety@springernature.com
ProductSafety@springernature.com

Poststr. 9
Darmstadt
64293
Deutschland