LEADER 04464nam 22007095 450 001 996465375403316 005 20240131165646.0 010 $a3-540-45616-3 024 7 $a10.1007/3-540-45616-3 035 $a(CKB)1000000000211784 035 $a(SSID)ssj0000321539 035 $a(PQKBManifestationID)11227089 035 $a(PQKBTitleCode)TC0000321539 035 $a(PQKBWorkID)10280761 035 $a(PQKB)11043503 035 $a(DE-He213)978-3-540-45616-2 035 $a(MiAaPQ)EBC3071738 035 $a(PPN)155218115 035 $a(EXLCZ)991000000000211784 100 $a20121227d2002 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Reasoning with Analytic Tableaux and Related Methods$b[electronic resource] $eInternational Conference, TABLEAUX 2002. Copenhagen, Denmark, July 30 - August 1, 2002. Proceedings /$fedited by Uwe Egly, Christian G. Fernmüller 205 $a1st ed. 2002. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2002. 215 $a1 online resource (X, 346 p.) 225 1 $aLecture Notes in Artificial Intelligence ;$v2381 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-43929-3 320 $aIncludes bibliographical references and index. 327 $aInvited Papers -- Proof Analysis by Resolution -- Using Linear Logic to Reason about Sequent Systems -- Research Papers -- A Schütte-Tait Style Cut-Elimination Proof for First-Order Gödel Logic -- Tableaux for Quantified Hybrid Logic -- Tableau-Based Automated Deduction for Duration Calculus -- Linear Time Logic, Conditioned Models, and Planning with Incomplete Knowledge -- A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic -- Modal Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks -- Tableau Calculi for the Logics of Finite k-Ary Trees -- A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition -- Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment -- Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas -- Integration of Equality Reasoning into the Disconnection Calculus -- Analytic Sequent Calculi for Abelian and ?ukasiewicz Logics -- Analytic Tableau Systems for Propositional Bimodal Logics of Knowledge and Belief -- A Confluent Theory Connection Calculus -- On Uniform Word Problems Involving Bridging Operators on Distributive Lattices -- Question Answering: From Partitions to Prolog -- A General Theorem Prover for Quantified Modal Logics -- Some New Exceptions for the Semantic Tableaux Version of the Second Incompleteness Theorem -- A New Indefinite Semantics for Hilbert?s Epsilon -- A Tableau Calculus for Combining Non-disjoint Theories -- System Descriptions Papers -- LINK: A Proof Environment Based on Proof Nets -- DCTP 1.2 ? System Abstract. 410 0$aLecture Notes in Artificial Intelligence ;$v2381 606 $aArtificial intelligence 606 $aMathematical logic 606 $aSoftware engineering 606 $aComputer programming 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 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 615 0$aArtificial intelligence. 615 0$aMathematical logic. 615 0$aSoftware engineering. 615 0$aComputer programming. 615 14$aArtificial Intelligence. 615 24$aMathematical Logic and Formal Languages. 615 24$aSoftware Engineering. 615 24$aProgramming Techniques. 676 $a006.3/33 702 $aEgly$b Uwe$f1960-$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aFernmüller$b Christian G$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTABLEAUX 2002 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465375403316 996 $aAutomated Reasoning with Analytic Tableaux and Related Methods$92556460 997 $aUNISA