LEADER 03165nam 2200577 450 001 996465913103316 005 20220423174526.0 010 $a3-540-73099-0 024 7 $a10.1007/978-3-540-73099-6 035 $a(CKB)1000000000490355 035 $a(SSID)ssj0000316401 035 $a(PQKBManifestationID)11273124 035 $a(PQKBTitleCode)TC0000316401 035 $a(PQKBWorkID)10276113 035 $a(PQKB)10195918 035 $a(DE-He213)978-3-540-73099-6 035 $a(MiAaPQ)EBC3063341 035 $a(MiAaPQ)EBC6694522 035 $a(Au-PeEL)EBL6694522 035 $a(PPN)123163005 035 $a(EXLCZ)991000000000490355 100 $a20220423d2007 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 00$aAutomated reasoning with analytic tableaux and related methods $einternational conference, TABLEAUX 2007, Aix en Provence, France, July 2007, proceedings /$fNicola Olivetti (editor) 205 $a1st ed. 2007. 210 1$aBerlin, Heidelberg :$cSpringer-Verlag,$d[2007] 210 4$dİ2007 215 $a1 online resource (X, 250 p.) 225 1 $aLecture Notes in Artificial Intelligence ;$v4548 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-73098-2 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- Nonmonotonic Description Logics ? Requirements, Theory, and Implementations -- Our Quest for the Holy Grail of Agent Verification -- An Abstract Framework for Satisfiability Modulo Theories -- Research Papers -- Axiom Pinpointing in General Tableaux -- Proof Theory for First Order ?ukasiewicz Logic -- A Tableau Method for Public Announcement Logics -- Bounded Model Checking with Description Logic Reasoning -- Tableau Systems for Logics of Subinterval Structures over Dense Orderings -- A Cut-Free Sequent Calculus for Bi-intuitionistic Logic -- Tableaux with Dynamic Filtration for Layered Modal Logics -- The Neighbourhood of S0.9 and S1 -- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies -- Tree-Sequent Methods for Subintuitionistic Predicate Logics -- A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation -- Updating Reduced Implicate Tries -- A Bottom-Up Approach to Clausal Tableaux -- Differential Dynamic Logic for Verifying Parametric Hybrid Systems -- System Descriptions -- Improvements to the Tableau Prover PITP -- KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning. 410 0$aLecture notes in computer science.$pLecture notes in artificial intelligence ;$v4548. 606 $aAutomatic theorem proving$vCongresses 606 $aAutomatic theorem proving 615 0$aAutomatic theorem proving 615 0$aAutomatic theorem proving. 676 $a004.015113 702 $aOlivetti$b Nicola 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465913103316 996 $aAutomated Reasoning with Analytic Tableaux and Related Methods$92556460 997 $aUNISA