LEADER 04563nam 22007455 450 001 996550548203316 005 20230913153417.0 010 $a3-031-43513-3 024 7 $a10.1007/978-3-031-43513-3 035 $a(CKB)5670000000770229 035 $a(DE-He213)978-3-031-43513-3 035 $a(PPN)272734403 035 $a(MiAaPQ)EBC30882876 035 $a(Au-PeEL)EBL30882876 035 $a(OCoLC)1398310890 035 $a(EXLCZ)995670000000770229 100 $a20230913d2023 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aAutomated Reasoning with Analytic Tableaux and Related Methods$b[electronic resource] $e32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18?21, 2023, Proceedings /$fedited by Revantha Ramanayake, Josef Urban 205 $a1st ed. 2023. 210 1$aCham :$cSpringer Nature Switzerland :$cImprint: Springer,$d2023. 215 $a1 online resource (XXV, 482 p. 370 illus., 12 illus. in color.) 225 1 $aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v14278 311 $a3-031-43512-5 327 $aRange-Restricted and Horn Interpolation through Clausal Tableaux -- Non-Classical Logics in Satisfiability Modulo Theories -- DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics -- Non-distributive description logic -- A new calculus for intuitionistic Strong L\"ob logic: strong termination and cut-elimination, formalized -- Some Analytic Systems of Rules -- A cut-free, sound and complete Russellian theory of definite descriptions -- Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators -- Lemmas: Generation, Selection, Application -- Machine-Learned Premise Selection for Lean -- gym-saturation: Gymnasium environments for saturation provers (System description) -- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points -- Ill-founded Proof Systems For Intuitionistic Linear-time Temporal Logic -- Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata -- Extensions of K5: Proof Theory and Uniform Lyndon Interpolation -- On intuitionistic diamonds (and lack thereof) -- NP Complexity for Combinations of Non-Normal Modal Logics -- Resolution-based Calculi for Non-Normal Modal Logics -- Canonicity of Proofs in Constructive Modal Logic -- Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic -- The MaxSAT problem in the real-valued MV-algebra -- The Logic of Separation Logic: Models and Proofs -- Testing the Satisfiability of Formulas in Separation Logic with Permissions -- Nested Sequents for Quantified Modal Logics -- A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness. 330 $aThis open access book constitutes the proceedings of the 32nd International Conference, TABLEAUX 2023, held in Prague, Czech Republic, during September 18?21, 2023. 410 0$aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v14278 606 $aArtificial intelligence 606 $aMachine theory 606 $aComputer science 606 $aSoftware engineering 606 $aComputer systems 606 $aMicroprogramming 606 $aArtificial Intelligence 606 $aFormal Languages and Automata Theory 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aComputer System Implementation 606 $aControl Structures and Microprogramming 615 0$aArtificial intelligence. 615 0$aMachine theory. 615 0$aComputer science. 615 0$aSoftware engineering. 615 0$aComputer systems. 615 0$aMicroprogramming. 615 14$aArtificial Intelligence. 615 24$aFormal Languages and Automata Theory. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aComputer System Implementation. 615 24$aControl Structures and Microprogramming. 676 $a006.3 702 $aRamanayake$b Revantha$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aUrban$b Josef$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996550548203316 996 $aAutomated Reasoning with Analytic Tableaux and Related Methods$92556460 997 $aUNISA