Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, Tableaux 2023, Prague, Czech Republic, September 18-21,

ISBN-13: 9783031435126 / Angielski

Revantha Ramanayake; Josef Urban

Spis treści

Range-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.

Blurb

This open access book constitutes the proceedings of the 32nd International Conference, TABLEAUX 2023, held in Prague, Czech Republic, during September 18–21, 2023.