---

＜電子ブック＞
5th Conference on Automated Deduction : Les Arcs, France, July 8-11, 1980 / edited by Wolfgang Bibel, R. Kowalski
(Lecture Notes in Computer Science. ISSN:16113349 ; 87)

版	1st ed. 1980.
出版者	Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer
出版年	1980
本文言語	英語
大きさ	VIII, 388 p : online resource
著者標目	Bibel, Wolfgang editor Kowalski, R editor SpringerLink (Online service)
件　名	LCSH:Mathematical logic LCSH:Machine theory FREE:Mathematical Logic and Foundations FREE:Formal Languages and Automata Theory
一般注記	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 HTTP:URL=https://doi.org/10.1007/3-540-10009-1

 類似資料