LEADER 03844nam 22006495 450 001 9910143638903321 005 20200702175918.0 010 $a3-540-46508-1 024 7 $a10.1007/3-540-46508-1 035 $a(CKB)1000000000211206 035 $a(SSID)ssj0000321528 035 $a(PQKBManifestationID)11227087 035 $a(PQKBTitleCode)TC0000321528 035 $a(PQKBWorkID)10280880 035 $a(PQKB)10116997 035 $a(DE-He213)978-3-540-46508-9 035 $a(MiAaPQ)EBC3072101 035 $a(PPN)155177648 035 $a(EXLCZ)991000000000211206 100 $a20121227d2000 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Deduction in Classical and Non-Classical Logics $eSelected Papers /$fedited by Ricardo Caferra, Gernot Salzer 205 $a1st ed. 2000. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2000. 215 $a1 online resource (VIII, 304 p.) 225 1 $aLecture Notes in Artificial Intelligence ;$v1761 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-67190-0 320 $aIncludes bibliographical references and index. 327 $aInvited Papers -- Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory -- Higher-Order Modal Logic?A Sketch -- Proving Associative-Commutative Termination Using RPO-Compatible Orderings -- Decision Procedures and Model Building or How to Improve Logical Information in Automated Deduction -- Replacement Rules with Definition Detection -- Contributed Papers -- On the Complexity of Finite Sorted Algebras -- A Further and Effective Liberalization of the ?-Rule in Free Variable Semantic Tableaux -- A New Fast Tableau-Based Decision Procedure for an Unquantified Fragment of Set Theory -- Interpretation of a Mizar-Like Logic in First Order Logic -- An ((n · log n)3)-Time Transformation from Grz into Decidable Fragments of Classical First-Order Logic -- Implicational Completeness of Signed Resolution -- An Equational Re-engineering of Set Theories -- Issues of Decidability for Description Logics in the Framework of Resolution -- Extending Decidable Clause Classes via Constraints -- Completeness and Redundancy in Constrained Clause Logic -- Effective Properties of Some First Order Intuitionistic Modal Logics -- Hidden Congruent Deduction -- Resolution-Based Theorem Proving for SH n-Logics -- Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized ?-Rule but Without Skolemization. 410 0$aLecture Notes in Artificial Intelligence ;$v1761 606 $aArtificial intelligence 606 $aMathematical logic 606 $aComputer logic 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 615 0$aArtificial intelligence. 615 0$aMathematical logic. 615 0$aComputer logic. 615 14$aArtificial Intelligence. 615 24$aMathematical Logic and Formal Languages. 615 24$aLogics and Meanings of Programs. 676 $a006.3/33 702 $aCaferra$b Ricardo$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSalzer$b Gernot$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910143638903321 996 $aAutomated deduction in classical and non-classical logics$91488828 997 $aUNINA