LEADER 05387nam 22006495 450 001 9910767560303321 005 20251117073002.0 010 $a3-540-45008-4 024 7 $a10.1007/10722086 035 $a(CKB)1000000000548797 035 $a(SSID)ssj0000321538 035 $a(PQKBManifestationID)11232826 035 $a(PQKBTitleCode)TC0000321538 035 $a(PQKBWorkID)10279782 035 $a(PQKB)10467648 035 $a(DE-He213)978-3-540-45008-5 035 $a(MiAaPQ)EBC3087414 035 $a(PPN)155196405 035 $a(BIP)13627350 035 $a(BIP)6530044 035 $a(EXLCZ)991000000000548797 100 $a20121227d2000 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Reasoning with Analytic Tableaux and Related Methods $eInternational Conference, TABLEAUX 2000 St Andrews, Scotland, UK, July 3-7, 2000 Proceedings /$fedited by Roy Dyckhoff 205 $a1st ed. 2000. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2000. 215 $a1 online resource (X, 440 p.) 225 1 $aLecture Notes in Artificial Intelligence ;$v1847 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-540-67697-X 320 $aIncludes bibliographical references. 327 $aInvited Lectures -- Tableau Algorithms for Description Logics -- Modality and Databases -- Local Symmetries in Propositional Logic -- Comparison -- Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison -- Consistency Testing: The RACE Experience -- Benchmark Analysis with FaCT -- MSPASS: Modal Reasoning by Translation and First-Order Resolution -- TANCS-2000 Results for DLP -- Evaluating *SAT on TANCS 2000 Benchmarks -- Research Papers -- A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations -- A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus -- An Analytic Calculus for Quantified Propositional Gödel Logic -- A Tableau Method for Inconsistency-Adaptive Logics -- A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning -- Hypertableau and Path-Hypertableau Calculi for some Families of Intermediate Logics -- Variants of First-Order Modal Logics -- Complexity of Simple Dependent Bimodal Logics -- Properties of Embeddings from Int to S4 -- Term-Modal Logics -- A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics -- Dual Intuitionistic Logic Revisited -- Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions -- Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints -- Matrix-Based Inductive Theorem Proving -- Monotonic Preorders for Free Variable Tableaux -- The Mosaic Method for Temporal Logics -- Sequent-Like Tableau Systems with the Analytic Superformula Property for the Modal Logics KB, KDB, K5, KD5 -- A Tableau Calculus for Equilibrium Entailment -- Towards Tableau-Based Decision Procedures for Non-Well-Founded Fragments of Set Theory -- Tableau Calculus for Only Knowing and Knowing At Most -- A Tableau-Like Representation Framework for Efficient Proof Reconstruction -- The Semantic Tableaux Version of the Second Incompleteness Theorem Extends Almost to Robinson?s Arithmetic Q -- System Descriptions -- Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO -- E-SETHEO: An Automated3 Theorem Prover. 330 $aThis book constitutes the refereed proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2000, held in St Andrews, Scotland, UK, in July 2000.The 23 revised full papers and 2 system descriptions presented were carefully reviewed and selected from 42 submissions. Also included are 3 invited lectures and 6 nonclassical system comparisons. All current issues surrounding the mechanization of reasoning with tableaux and similar methods are addressed - ranging from theoretical foundations to implementation, systems development, and applications, as well as covering a broad variety of logical calculi. 410 0$aLecture Notes in Artificial Intelligence ;$v1847 606 $aArtificial intelligence 606 $aProgramming languages (Electronic computers) 606 $aLogic, Symbolic and mathematical 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aArtificial intelligence. 615 0$aProgramming languages (Electronic computers) 615 0$aLogic, Symbolic and mathematical. 615 14$aArtificial Intelligence. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aMathematical Logic and Formal Languages. 676 $a006.3/33 702 $aDyckhoff$b Roy$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTABLEAUX 2000 906 $aBOOK 912 $a9910767560303321 996 $aAutomated Reasoning with Analytic Tableaux and Related Methods$92556460 997 $aUNINA