---

＜電子ブック＞
6th Conference on Automated Deduction : New York, USA, June 7-9, 1982 / edited by D. W. Loveland
(Lecture Notes in Computer Science. ISSN:16113349 ; 138)

版	1st ed. 1982.
出版者	(Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer)
出版年	1982
本文言語	英語
大きさ	VII, 389 p : online resource
著者標目	Loveland, D. W editor SpringerLink (Online service)
件　名	LCSH:Machine theory FREE:Formal Languages and Automata Theory
一般注記	Solving open questions with an automated theorem-proving program -- STP: A mechanized logic for specification and verification -- A look at TPS -- Logic machine architecture: Kernel functions -- Logic machine architecture: Inference mechanisms -- Procedure implementation through demodulation and related tricks -- The application of Homogenization to simultaneous equations -- Meta-level inference and program verification -- An example of FOL using metatheory -- Comparison of natural deduction and locking resolution implementations -- Derived preconditions and their use in program synthesis -- Automatic construction of special purpose programs -- Deciding combinations of theories -- Exponential improvement of efficient backtracking -- Exponential improvement of exhaustive backtracking: data structure and implementation -- Intuitionistic basis for non-monotonic logic -- Knowledge retrieval as limited inference -- On indefinite databases and the closed world assumption -- Proof by matrix reduction as plan + validation -- Improvements of a tautology-testing algorithm -- Representing infinite sequences of resolvents in recursive First-Order Horn Databases -- The power of the Church-Rosser property for string rewriting systems -- Universal unification and a classification of equational theories HTTP:URL=https://doi.org/10.1007/BFb0000048

 類似資料