LEADER 03026nam  22004815  450 
001 996466349003316
005 20200701034024.0
010   $a3-540-39240-8
024 7 $a10.1007/BFb0000048
035   $a(CKB)1000000000230184
035   $a(SSID)ssj0000320751
035   $a(PQKBManifestationID)11256866
035   $a(PQKBTitleCode)TC0000320751
035   $a(PQKBWorkID)10249371
035   $a(PQKB)11534217
035   $a(DE-He213)978-3-540-39240-8
035   $a(PPN)15521005X
035   $a(EXLCZ)991000000000230184
100   $a20121227d1982      u|             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$a6th Conference on Automated Deduction$b[electronic resource] $eNew York, USA, June 7-9, 1982 /$fedited by D. W. Loveland
205   $a1st ed. 1982.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1982.
215   $a1 online resource (VII, 389 p.)
225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v138
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-11558-7 
327   $aSolving 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.
410  0$aLecture Notes in Computer Science,$x0302-9743 ;$v138
606   $aMathematical logic
606   $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048
615  0$aMathematical logic.
615 14$aMathematical Logic and Formal Languages.
676   $a005.131
702   $aLoveland$b D. W$4edt$4http://id.loc.gov/vocabulary/relators/edt
906   $aBOOK
912   $a996466349003316
996   $a6th Conference on Automated Deduction$92830824
997   $aUNISA