


default search action
30th TABLEAUX 2021: Birmingham, UK
- Anupam Das, Sara Negri:
Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings. Lecture Notes in Computer Science 12842, Springer 2021, ISBN 978-3-030-86058-5
Tableau Calculi
- Thomas Macaulay Ferguson
:
Tableaux and Restricted Quantification for Systems Related to Weak Kleene Logic. 3-19 - Marta Bílková
, Sabine Frittella
, Daniil Kozhemiachenko
:
Constraint Tableaux for Two-Dimensional Fuzzy Logics. 20-37 - Lukas Grätz
:
Analytic Tableaux for Non-deterministic Semantics. 38-55 - Andrzej Indrzejczak
, Michal Zawidzki
:
Tableaux for Free Logics with Descriptions. 56-73 - Rajeev Goré, Cormac Kikkert
:
CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-Learning and SAT. 74-91
Sequent Calculi
- Nils Kürbis
:
Proof-Theory and Semantics for a Theory of Definite Descriptions. 95-111 - Arnon Avron
:
Basing Sequent Systems on Exclusive-Or. 112-128 - Vitor Greati
, Sérgio Marcelino
, João Marcos
:
Proof Search on Bilateralist Judgments over Non-deterministic Semantics. 129-146 - Björn Lellmann
:
From Input/Output Logics to Conditional Logics via Sequents - with Provers. 147-164
Theorem Proving
- Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban:
Towards Finding Longer Proofs. 167-186 - Michael Rawson, Giles Reger:
lazyCoP: Lazy Paramodulation Meets Neurally Guided Search. 187-199 - André Duarte
, Konstantin Korovin
:
AC Simplifications and Closure Redundancies in the Superposition Calculus. 200-217 - Zsolt Zombori, Josef Urban, Miroslav Olsák:
The Role of Entropy in Guiding a Connection Prover. 218-235 - Jens Otten
:
The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics. 236-249 - Michael Rawson, Giles Reger:
Eliminating Models During Model Elimination. 250-265 - Karel Chvalovský
, Jan Jakubuv
, Miroslav Olsák
, Josef Urban
:
Learning Theorem Proving Components. 266-278
Formalized Proofs
- Caitlin D'Abrera
, Jeremy E. Dawson
, Rajeev Goré:
A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic. 281-298 - Rajeev Goré, Revantha Ramanayake
, Ian Shillito
:
Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq. 299-313
Non-Wellfounded Proofs
- Stepan L. Kuznetsov
:
Complexity of a Fragment of Infinitary Action Logic with Exponential via Non-well-founded Proofs. 317-334 - Bahareh Afshari, Graham E. Leigh
, Guillermo Menéndez Turata:
Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus. 335-353 - Jan Rooduijn:
Cyclic Hypersequent Calculi for Some Modal Logics with the Master Modality. 354-370 - Johannes Marti, Yde Venema:
A Focus System for the Alternation-Free μ-Calculus. 371-388
Intuitionistic Modal Logics
- Tiziano Dalmonte
, Charles Grellois
, Nicola Olivetti
:
Terminating Calculi and Countermodels for Constructive Modal Logics. 391-408 - Tim S. Lyon
:
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement. 409-427 - Matteo Acclavio
, Davide Catta, Lutz Straßburger:
Game Semantics for Constructive Modal Logic. 428-445 - Michael Mendler, Stephan Scheele, Luke Burke:
The Došen Square Under Construction: A Tale of Four Modalities. 446-465

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.