このページのリンク

<電子ブック>
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
目次/あらすじ

所蔵情報を非表示

電子ブック オンライン 電子ブック


Springer eBooks 9783540381402
電子リソース
EB00224752

書誌詳細を非表示

データ種別 電子ブック
分 類 LCC:QA8.9-10.3
DC23:511.3
書誌ID 4001088561
ISBN 9783540381402

 類似資料