Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
55 | Norbert E. Fuchs, Uta Schwertel, Sunna Torge 0001 |
Controlled Natural Language Can Replace First-Order Logic. |
ASE |
1999 |
DBLP DOI BibTeX RDF |
Attempto Controlled English, EP Tableaux, database schema design, Schubert's Steamroller, formal methods, model generation, controlled natural language, automatic reasoning |
51 | Leopoldo E. Bertossi, Camilla Schwind |
Analytic Tableaux and Database Repairs: Foundations. |
FoIKS |
2002 |
DBLP DOI BibTeX RDF |
|
51 | Giuseppe De Giacomo, Fabio Massacci |
Tableaux and Algorithms for Propositional Dynamic Logic with Converse. |
CADE |
1996 |
DBLP DOI BibTeX RDF |
|
51 | Fabio Massacci |
Strongly Analytic Tableaux for Normal Modal Logics. |
CADE |
1994 |
DBLP DOI BibTeX RDF |
|
51 | Joanna Golinska-Pilarek, Ewa Orlowska |
Tableaux and Dual Tableaux: Transformation of Proofs. |
Stud Logica |
2007 |
DBLP DOI BibTeX RDF |
first-order logic with identity, tableaux systems, Rasiowa-Sikorski proof system |
48 | Slim Abdennadher, Heribert Schütz |
Model Generation with Existentially Quantified Variables and Constraints. |
ALP/HOA |
1997 |
DBLP DOI BibTeX RDF |
|
48 | Jens Otten, Wolfgang Bibel (eds.) |
Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) affiliated with the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023), Prague, Czech Republic, September 18, 2023. |
AReCCa@TABLEAUX |
2024 |
DBLP BibTeX RDF |
|
48 | Revantha Ramanayake, Josef Urban (eds.) |
Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Ineke van der Berg, Andrea De Domenico, Giuseppe Greco 0001, Krishna Manoorkar, Alessandra Palmigiano, Mattia Panettiere |
Non-distributive Description Logic. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Dirk Pattinson, Nicola Olivetti, Cláudia Nalon |
Resolution Calculi for Non-normal Modal Logics. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Bartosz Piotrowski, Ramon Fernández Mir, Edward W. Ayers |
Machine-Learned Premise Selection for Lean. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Michael Rawson 0001, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel |
Lemmas: Generation, Selection, Application. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Zuzana Haniková, Felip Manyà, Amanda Vidal |
The MaxSAT Problem in the Real-Valued MV-Algebra. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Tim S. Lyon, Eugenio Orlandelli |
Nested Sequents for Quantified Modal Logics. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Alexander V. Gheorghiu, Tao Gu, David J. Pym |
Proof-Theoretic Semantics for Intuitionistic Multiplicative Linear Logic. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Iris van der Giessen, Raheleh Jalali, Roman Kuznets |
Extensions of K5: Proof Theory and Uniform Lyndon Interpolation. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | 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. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Andrzej Indrzejczak |
Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Maurice Dekker, Johannes Kloibhofer, Johannes Marti, Yde Venema |
Proof Systems for the Modal μ-Calculus Obtained by Determinizing Automata. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Boris Shminke |
gym-saturation: Gymnasium Environments for Saturation Provers (System description). |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Anupam Das 0002, Sonia Marin |
On Intuitionistic Diamonds (and Lack Thereof). |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Nicolas Peltier |
Testing the Satisfiability of Formulas in Separation Logic with Permissions. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Bahareh Afshari, Lide Grotenhuis, Graham E. Leigh, Lukas Zenger |
Ill-Founded Proof Systems for Intuitionistic Linear-Time Temporal Logic. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Matteo Acclavio, Davide Catta, Federico Olimpieri |
Canonicity of Proofs in Constructive Modal Logic. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Alexis Saurin |
A Linear Perspective on Cut-Elimination for Non-wellfounded Sequent Calculi with Least and Greatest Fixed-Points. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Andrzej Indrzejczak, Nils Kürbis |
A Cut-Free, Sound and Complete Russellian Theory of Definite Descriptions. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Frank S. de Boer, Hans-Dieter A. Hiep, Stijn de Gouw |
The Logic of Separation Logic: Models and Proofs. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Timo Lang |
Some Analytic Systems of Rules. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Tiziano Dalmonte, Andrea Mazzullo |
CoNP Complexity for Combinations of Non-normal Modal Logics. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Asta Halkjær From, Jørgen Villadsen |
A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Clemens Eisenhofer, Ruba Alassaf, Michael Rawson 0001, Laura Kovács |
Non-Classical Logics in Satisfiability Modulo Theories. |
TABLEAUX |
2023 |
DBLP DOI BibTeX RDF |
|
48 | |
Preface. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Leo Repp, Mario Frank 0002 |
nanoCoP-Omega: A Non-Clausal Connection Prover with Arithmetic. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Sean B. Holden |
Connect++: A New Automated Theorem Prover Based on the Connection Calculus. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Jens Otten, Sean B. Holden |
A Syntax for Connection Proofs. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Wolfgang Bibel |
Comparison of Proof Methods. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Clemens Eisenhofer, Laura Kovács, Michael Rawson 0001 |
Embedding the Connection Calculus in Satisfiability Modulo Theories. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Christoph Wernhard |
Structure-Generating First-Order Theorem Proving. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Jens Otten |
20 Years of leanCoP - An Overview of the Provers. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Fredrik Rømming, Jens Otten, Sean B. Holden |
Connections: Markov Decision Processes for Classical, Intuitionistic and Modal Connection Calculi. |
AReCCa@TABLEAUX |
2023 |
DBLP BibTeX RDF |
|
48 | Anupam Das 0002, Sara Negri (eds.) |
Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Rajeev Goré, Revantha Ramanayake, Ian Shillito |
Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Jan Rooduijn |
Cyclic Hypersequent Calculi for Some Modal Logics with the Master Modality. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Nils Kürbis |
Proof-Theory and Semantics for a Theory of Definite Descriptions. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban |
Learning Theorem Proving Components. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Tim S. Lyon |
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Johannes Marti, Yde Venema |
A Focus System for the Alternation-Free μ-Calculus. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Vitor Greati, Sérgio Marcelino, João Marcos 0001 |
Proof Search on Bilateralist Judgments over Non-deterministic Semantics. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Arnon Avron |
Basing Sequent Systems on Exclusive-Or. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Björn Lellmann |
From Input/Output Logics to Conditional Logics via Sequents - with Provers. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban |
Towards Finding Longer Proofs. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Michael Mendler, Stephan Scheele, Luke Burke |
The Došen Square Under Construction: A Tale of Four Modalities. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Jens Otten |
The nanoCoP 2.0 Connection Provers for Classical, Intuitionistic and Modal Logics. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Matteo Acclavio, Davide Catta, Lutz Straßburger |
Game Semantics for Constructive Modal Logic. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Zsolt Zombori, Josef Urban, Miroslav Olsák |
The Role of Entropy in Guiding a Connection Prover. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Bahareh Afshari, Graham E. Leigh, Guillermo Menéndez Turata |
Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Tiziano Dalmonte, Charles Grellois, Nicola Olivetti |
Terminating Calculi and Countermodels for Constructive Modal Logics. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Michael Rawson 0001, Giles Reger |
Eliminating Models During Model Elimination. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | André Duarte 0002, Konstantin Korovin |
AC Simplifications and Closure Redundancies in the Superposition Calculus. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Caitlin D'Abrera, Jeremy E. Dawson, Rajeev Goré |
A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Michael Rawson 0001, Giles Reger |
lazyCoP: Lazy Paramodulation Meets Neurally Guided Search. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Stepan L. Kuznetsov |
Complexity of a Fragment of Infinitary Action Logic with Exponential via Non-well-founded Proofs. |
TABLEAUX |
2021 |
DBLP DOI BibTeX RDF |
|
48 | Serenella Cerrito, Andrei Popescu 0001 (eds.) |
Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Simon Docherty, Reuben N. S. Rowe |
A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Daniel Gâinâ, Ionut Tutu |
Birkhoff Completeness for Hybrid-Dynamic First-Order Logic. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Elaine Pimentel, Revantha Ramanayake, Björn Lellmann |
Sequentialising Nested Systems. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Ioana Leustean, Natalia Moanga, Traian-Florin Serbanuta |
Operational Semantics and Program Verification Using Many-Sorted Hybrid Modal Logic. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Benjamin Ralph, Lutz Straßburger |
Towards a Combinatorial Proof Theory. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Agata Ciabattoni, Timo Lang, Revantha Ramanayake |
Bounded Sequent Calculi for Non-classical Logics via Hypersequents. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Abhishek De 0001, Alexis Saurin |
Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Luca Geatti, Nicola Gigante, Angelo Montanari |
A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Timo Lang, Carlos Olarte, Elaine Pimentel, Christian G. Fermüller |
A Game Model for Proofs with Costs. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Gabriel Ebner |
Herbrand Constructivization for Automated Intuitionistic Theorem Proving. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Björn Lellmann |
Combining Monotone and Normal Modal Logic in Nested Sequents - with Countermodels. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Eduard Kamburjan |
Behavioral Program Logic. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Chu Min Li, Felip Manyà, Joan Ramon Soler |
A Tableau Calculus for Non-clausal Maximum Satisfiability. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban |
ENIGMAWatch: ProofWatch Meets ENIGMA. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Anthony Lick |
A Hypersequent Calculus with Clusters for Data Logic over Ordinals. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Didier Galmiche, Michel Marti, Daniel Méry |
Relating Labelled and Label-Free Bunched Calculi in BI Logic. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Matteo Acclavio, Lutz Straßburger |
On Combinatorial Proofs for Modal Logic. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | João G. Martins, André Platzer, João Leite 0001 |
Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Rajeev Goré, Björn Lellmann |
Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Mnacho Echenim, Radu Iosif, Nicolas Peltier |
Prenex Separation Logic with One Selector Field. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Camillo Fiorentini, Rajeev Goré, Stéphane Graham-Lengrand |
A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Yotam Dvir, Arnon Avron |
First-Order Quasi-canonical Proof Systems. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Rémi Nollet, Alexis Saurin, Christine Tasson |
PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest Fixed Points. |
TABLEAUX |
2019 |
DBLP DOI BibTeX RDF |
|
48 | Renate A. Schmidt, Cláudia Nalon (eds.) |
Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Marianna Girlando, Björn Lellmann, Nicola Olivetti, Gian Luca Pozzato |
Hypersequent Calculi for Lewis' Conditional Logics with Uniformity and Reflexivity. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | David M. Cerna, Michael Peter Lettmann |
Integrating a Global Induction Mechanism into a Sequent Calculus. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Anupam Das 0002, Damien Pous |
A Cut-Free Cyclic Proof System for Kleene Algebra. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Jens Otten |
Non-clausal Connection Calculi for Non-classical Logics. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Crystal Chang Din, Reiner Hähnle, Einar Broch Johnsen, Ka I Pun, Silvia Lizeth Tapia Tarifa |
Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Peter H. Schmitt |
A Mechanizable First-Order Theory of Ordinals. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Sonia Marin, Lutz Straßburger |
Proof Theory for Indexed Nested Sequents. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Jeremy E. Dawson, Rajeev Goré |
Issues in Machine-Checking the Decidability of Implicational Ticket Entailment. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Liron Cohen 0001 |
Completeness for Ancestral Logic via a Computationally-Meaningful Semantics. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Mateus de Oliveira Oliveira |
Parameterized Provability in Equational Logic. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Sorin Stratulat |
Cyclic Proofs with Ordering Constraints. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Dmitry Tishkovsky, Renate A. Schmidt |
Rule Refinement for Semantic Tableau Calculi. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
48 | Camillo Fiorentini, Mauro Ferrari 0002 |
A Forward Unprovability Calculus for Intuitionistic Propositional Logic. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|