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.