001480683 000__ 04371cam\\22005897i\4500 001480683 001__ 1480683 001480683 003__ OCoLC 001480683 005__ 20231031003304.0 001480683 006__ m\\\\\o\\d\\\\\\\\ 001480683 007__ cr\cn\nnnunnun 001480683 008__ 230920s2023\\\\sz\\\\\\o\\\\\000\0\eng\d 001480683 019__ $$a1402834310$$a1405397385 001480683 020__ $$a9783031435133$$q(electronic bk.) 001480683 020__ $$a3031435133$$q(electronic bk.) 001480683 020__ $$z9783031435126 001480683 0247_ $$a10.1007/978-3-031-43513-3$$2doi 001480683 035__ $$aSP(OCoLC)1398310890 001480683 040__ $$aGW5XE$$beng$$erda$$epn$$cGW5XE$$dSFB$$dWSU 001480683 049__ $$aISEA 001480683 050_4 $$aQA76.9.A96$$bT33 2023eb 001480683 08204 $$a511.3/6028563$$223/eng/20230920 001480683 1112_ $$aTABLEAUX (Conference)$$n(32nd :$$d2023 :$$cPrague, Czech Republic) 001480683 24510 $$aAutomated reasoning with analytic tableaux and related methods :$$b32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings /$$cRevantha Ramanayake, Josef Urban, editors. 001480683 2463_ $$aTABLEAUX 2023 001480683 264_1 $$aCham :$$bSpringer,$$c2023. 001480683 300__ $$a1 online resource (xxv, 482 pages) :$$billustrations (some color). 001480683 336__ $$atext$$btxt$$2rdacontent 001480683 337__ $$acomputer$$bc$$2rdamedia 001480683 338__ $$aonline resource$$bcr$$2rdacarrier 001480683 4901_ $$aLecture notes in artificial intelligence 001480683 4901_ $$aLecture notes in computer science ;$$v14278 001480683 4901_ $$aLNCS Sublibrary, SL 7, Artificial intelligence 001480683 5050_ $$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. 001480683 5060_ $$aOpen access.$$5GW5XE 001480683 520__ $$aThis open access book constitutes the proceedings of the 32nd International Conference, TABLEAUX 2023, held in Prague, Czech Republic, during September 18-21, 2023. 001480683 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed September 20, 2023). 001480683 650_0 $$aAutomatic theorem proving$$vCongresses. 001480683 655_7 $$aConference papers and proceedings.$$2lcgft 001480683 655_0 $$aElectronic books. 001480683 7001_ $$aRamanayake, Revantha,$$eeditor.$$0(orcid)0000-0002-7940-9065$$1https://orcid.org/0000-0002-7940-9065 001480683 7001_ $$aUrban, Josef,$$eeditor.$$0(orcid)0000-0002-1384-1613$$1https://orcid.org/0000-0002-1384-1613 001480683 830_0 $$aLecture notes in computer science.$$pLecture notes in artificial intelligence. 001480683 830_0 $$aLecture notes in computer science ;$$v14278. 001480683 830_0 $$aLNCS sublibrary.$$nSL 7,$$pArtificial intelligence. 001480683 852__ $$bebk 001480683 85640 $$3Springer Nature$$uhttps://link.springer.com/10.1007/978-3-031-43513-3$$zOnline Access$$91397441.2 001480683 909CO $$ooai:library.usi.edu:1480683$$pGLOBAL_SET 001480683 980__ $$aBIB 001480683 980__ $$aEBOOK 001480683 982__ $$aEbook 001480683 983__ $$aOnline 001480683 994__ $$a92$$bISE