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

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

Bibliographic Details
Corporate Author:	SpringerLink (Online service)
Other Authors:	Ramanayake, Revantha (Editor), Urban, Josef (Editor)
Format:	eBook
Language:	English
Published:	Cham : Springer Nature Switzerland : Imprint: Springer, 2023.
Edition:	1st ed. 2023.
Series:	Lecture Notes in Artificial Intelligence, 14278
Subjects:	Artificial intelligence. Machine theory. Computer science. Software engineering. Computer systems. Microprogramming . Artificial Intelligence. Formal Languages and Automata Theory. Computer Science Logic and Foundations of Programming. Software Engineering. Computer System Implementation. Control Structures and Microprogramming. Electronic books.
Online Access:	Connect to the full text of this electronic book

Table of Contents:

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.