03871nam 22006495 450 991014363890332120200702175918.03-540-46508-110.1007/3-540-46508-1(CKB)1000000000211206(SSID)ssj0000321528(PQKBManifestationID)11227087(PQKBTitleCode)TC0000321528(PQKBWorkID)10280880(PQKB)10116997(DE-He213)978-3-540-46508-9(MiAaPQ)EBC3072101(PPN)155177648(EXLCZ)99100000000021120620121227d2000 u| 0engurnn|008mamaatxtccrAutomated Deduction in Classical and Non-Classical Logics[electronic resource] Selected Papers /edited by Ricardo Caferra, Gernot Salzer1st ed. 2000.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2000.1 online resource (VIII, 304 p.) Lecture Notes in Artificial Intelligence ;1761Bibliographic Level Mode of Issuance: Monograph3-540-67190-0 Includes bibliographical references and index.Invited 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.Lecture Notes in Artificial Intelligence ;1761Artificial intelligenceMathematical logicComputer logicArtificial Intelligencehttps://scigraph.springernature.com/ontologies/product-market-codes/I21000Mathematical Logic and Formal Languageshttps://scigraph.springernature.com/ontologies/product-market-codes/I16048Logics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XArtificial intelligence.Mathematical logic.Computer logic.Artificial Intelligence.Mathematical Logic and Formal Languages.Logics and Meanings of Programs.006.3/33Caferra Ricardoedthttp://id.loc.gov/vocabulary/relators/edtSalzer Gernotedthttp://id.loc.gov/vocabulary/relators/edtMiAaPQMiAaPQMiAaPQBOOK9910143638903321Automated deduction in classical and non-classical logics1488828UNINA