


default search action
32nd TABLEAUX 2023: Prague, Czech Republic
- Revantha Ramanayake

, Josef Urban
:
Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings. Lecture Notes in Computer Science 14278, Springer 2023, ISBN 978-3-031-43512-6
Tableau Calculi
- Christoph Wernhard

:
Range-Restricted and Horn Interpolation through Clausal Tableaux. 3-23 - Clemens Eisenhofer

, Ruba Alassaf
, Michael Rawson
, Laura Kovács
:
Non-Classical Logics in Satisfiability Modulo Theories. 24-36 - Carlos Areces

, Valentin Cassano, Raul Fervari, Guillaume Hoffmann:
DefTab : A Tableaux System for Sceptical Consequence in Default Modal Logics. 37-48 - Ineke van der Berg

, Andrea De Domenico
, Giuseppe Greco
, Krishna Manoorkar
, Alessandra Palmigiano
, Mattia Panettiere
:
Non-distributive Description Logic. 49-69
Sequent Calculi
- Ian Shillito

, Iris van der Giessen, Rajeev Goré, Rosalie Iemhoff
:
A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised. 73-93 - Timo Lang:

Some Analytic Systems of Rules. 94-111 - Andrzej Indrzejczak

, Nils Kürbis
:
A Cut-Free, Sound and Complete Russellian Theory of Definite Descriptions. 112-130 - Andrzej Indrzejczak

:
Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators. 131-149
Theorem Proving
- Michael Rawson

, Christoph Wernhard
, Zsolt Zombori
, Wolfgang Bibel
:
Lemmas: Generation, Selection, Application. 153-174 - Bartosz Piotrowski, Ramon Fernández Mir

, Edward W. Ayers:
Machine-Learned Premise Selection for Lean. 175-186 - Boris Shminke

:
gym-saturation: Gymnasium Environments for Saturation Provers (System description). 187-199
Non-wellfounded Proofs
- Alexis Saurin:

A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent Calculi with Least and Greatest Fixed-Points. 203-222 - Bahareh Afshari, Lide Grotenhuis, Graham E. Leigh

, Lukas Zenger
:
Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic. 223-241 - Maurice Dekker, Johannes Kloibhofer, Johannes Marti, Yde Venema:

Proof Systems for the Modal μ-Calculus Obtained by Determinizing Automata. 242-259
Modal Logics
- Iris van der Giessen, Raheleh Jalali

, Roman Kuznets
:
Extensions of K5: Proof Theory and Uniform Lyndon Interpolation. 263-282 - Anupam Das, Sonia Marin:

On Intuitionistic Diamonds (and Lack Thereof). 283-301 - Tiziano Dalmonte

, Andrea Mazzullo
:
CoNP Complexity for Combinations of Non-normal Modal Logics. 302-321 - Dirk Pattinson

, Nicola Olivetti
, Cláudia Nalon
:
Resolution Calculi for Non-normal Modal Logics. 322-341 - Matteo Acclavio

, Davide Catta, Federico Olimpieri:
Canonicity of Proofs in Constructive Modal Logic. 342-363
Linear Logic and MV-Algebras
- Alexander V. Gheorghiu

, Tao Gu
, David J. Pym
:
Proof-Theoretic Semantics for Intuitionistic Multiplicative Linear Logic. 367-385 - Zuzana Haniková

, Felip Manyà
, Amanda Vidal
:
The MaxSAT Problem in the Real-Valued MV-Algebra. 386-404
Separation Logic
- Frank S. de Boer, Hans-Dieter A. Hiep

, Stijn de Gouw:
The Logic of Separation Logic: Models and Proofs. 407-426 - Nicolas Peltier:

Testing the Satisfiability of Formulas in Separation Logic with Permissions. 427-445
First-Order Logics
- Tim S. Lyon

, Eugenio Orlandelli
:
Nested Sequents for Quantified Modal Logics. 449-467 - Asta Halkjær From

, Jørgen Villadsen
:
A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness. 468-480

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














