| Publication | Date of Publication | Type |
|---|
Machine-checked meta-theory of dual-tableaux for intuitionistic logic
| 2024-09-06 | Paper |
A new calculus for intuitionistic Strong L\"ob logic: strong termination and cut-elimination, formalised
| 2023-09-01 | Paper |
Tableau metatheory for syllogistic logics
| 2023-03-29 | Paper |
scientific article; zbMATH DE number 7668109 (Why is no real title available?)
| 2023-03-24 | Paper |
scientific article; zbMATH DE number 7650841 (Why is no real title available?)
| 2023-02-07 | Paper |
Verified Decision Procedures for Modal Logics.
| 2023-02-03 | Paper |
N-PAT: A Nested Model-Checker
Automated Reasoning | 2022-11-09 | Paper |
scientific article; zbMATH DE number 7585718 (Why is no real title available?)
| 2022-09-15 | Paper |
CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT
| 2022-05-25 | Paper |
A formally verified cut-elimination procedure for linear nested sequents for tense logic
| 2022-05-25 | Paper |
Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
| 2022-05-25 | Paper |
Machine-checked proof-theory for propositional modal logics
Advances in Proof Theory | 2020-08-07 | Paper |
A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
| 2020-05-14 | Paper |
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents
| 2020-05-14 | Paper |
A correct polynomial translation of S4 into intuitionistic logic
Journal of Symbolic Logic | 2020-04-06 | Paper |
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
| 2019-10-11 | Paper |
A labelled sequent calculus for BBI: proof theory and proof search
Journal Of Logic And Computation | 2019-01-31 | Paper |
Free variable tableaux for propositional modal logics
Lecture Notes in Computer Science | 2019-01-15 | Paper |
Well-founded unions
| 2018-10-18 | Paper |
Modular labelled sequent calculi for abstract separation logics
ACM Transactions on Computational Logic | 2018-08-10 | Paper |
Issues in machine-checking the decidability of implicational ticket entailment
| 2018-02-02 | Paper |
Yablo's paradox as a theorem of modal logic
| 2017-07-25 | Paper |
Annotation-free sequent calculi for full intuitionistic linear logic
| 2017-02-02 | Paper |
Machine-checked interpolation theorems for substructural logics using display calculi
Automated Reasoning | 2016-09-05 | Paper |
Automated theorem proving for assertions in separation logic with all connectives
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Sequent Calculus in the Topos of Trees
Lecture Notes in Computer Science | 2015-10-01 | Paper |
The Tableau Workbench
Electronic Notes in Theoretical Computer Science | 2015-03-23 | Paper |
An on-the-fly tableau-based decision procedure for PDL-satisfiability
Electronic Notes in Theoretical Computer Science | 2015-03-23 | Paper |
A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description
Automated Reasoning | 2014-09-26 | Paper |
And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL
Automated Reasoning | 2014-09-26 | Paper |
Implementing tableau calculi using BDDs: BDDTab system description
Automated Reasoning | 2014-09-26 | Paper |
From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
Advanced Information Systems Engineering | 2014-09-15 | Paper |
Cut-elimination for weak Grzegorczyk logic Go
Studia Logica | 2014-06-19 | Paper |
Labelled tree sequents, tree hypersequents and nested (deep) sequents
| 2014-06-11 | Paper |
scientific article; zbMATH DE number 6302922 (Why is no real title available?)
| 2014-06-11 | Paper |
Proof search for propositional abstract separation logics via labelled sequents
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Computer-aided decision-making with trust relations and trust domains (cryptographic applications)
Journal Of Logic And Computation | 2014-04-01 | Paper |
A labelled sequent calculus for BBI: proof theory and proof search
Lecture Notes in Computer Science | 2013-10-04 | Paper |
A new machine-checked proof of strong normalisation for display logic
| 2013-08-27 | Paper |
ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
Journal of Automated Reasoning | 2013-07-05 | Paper |
An improved BDD method for intuitionistic propositional logic: BDDIntKt system description
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
Analysing vote counting algorithms via logic. And its application to the CADE election scheme
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
BDD-based automated reasoning for propositional bi-intuitionistic tense logics
Automated Reasoning | 2012-09-05 | Paper |
Cut-elimination and proof search for bi-intuitionistic tense logic
| 2012-08-05 | Paper |
Valentini's cut-elimination for provability logic resolved
The Review of Symbolic Logic | 2012-06-11 | Paper |
Craig interpolation in displayable logics
Lecture Notes in Computer Science | 2011-07-01 | Paper |
On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
Logical Methods in Computer Science | 2011-05-26 | Paper |
Valentini's cut-elimination for provability logic resolved
| 2011-03-30 | Paper |
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents
| 2011-03-30 | Paper |
Generic methods for formalising sequent calculi applied to provability logic
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
A proof theoretic analysis of intruder theories
Logical Methods in Computer Science | 2010-09-21 | Paper |
Global caching for coalgebraic description logics
Automated Reasoning | 2010-09-14 | Paper |
Optimal and cut-free tableaux for propositional dynamic logic with converse
Automated Reasoning | 2010-09-14 | Paper |
Optimal tableau algorithms for coalgebraic logics
Tools and Algorithms for the Construction and Analysis of Systems | 2010-04-27 | Paper |
The tableaux work bench
Lecture Notes in Computer Science | 2010-03-09 | Paper |
Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic
Journal Of Logic And Computation | 2010-02-19 | Paper |
Completeness of hyper-resolution via the semantics of disjunctive logic programs
Information Processing Letters | 2009-12-04 | Paper |
Sound global state caching for ALC with inverse roles
Lecture Notes in Computer Science | 2009-12-01 | Paper |
Taming displayed tense logics using nested sequents with deep inference
Lecture Notes in Computer Science | 2009-12-01 | Paper |
Clausal Tableaux for Multimodal Logics of Belief
Fundamenta Informaticae | 2009-09-22 | Paper |
A First-Order Policy Language for History-Based Transaction Monitoring
Theoretical Aspects of Computing - ICTAC 2009 | 2009-08-20 | Paper |
An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
A Proof Theoretic Analysis of Intruder Theories
Rewriting Techniques and Applications | 2009-06-30 | Paper |
TERMINATION OF ABSTRACT REDUCTION SYSTEMS
International Journal of Foundations of Computer Science | 2009-04-14 | Paper |
Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
Lecture Notes in Computer Science | 2009-02-12 | Paper |
Machine Checking Proof Theory: An Application of Logic to Logic
Logic and Its Applications | 2009-02-12 | Paper |
An Experimental Evaluation of Global Caching for $\mathcal {ALC}$ (System Description)
Automated Reasoning | 2008-11-27 | Paper |
One-Pass Tableaux for Computation Tree Logic
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
Lecture Notes in Computer Science | 2008-01-04 | Paper |
A Cut-Free Sequent Calculus for Bi-intuitionistic Logic
Lecture Notes in Computer Science | 2008-01-04 | Paper |
Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5
Journal Of Logic And Computation | 2007-11-19 | Paper |
Automated Reasoning with Analytic Tableaux and Related Methods
Lecture Notes in Computer Science | 2006-07-07 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2005-08-22 | Paper |
Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
Lecture Notes in Computer Science | 2005-08-19 | Paper |
scientific article; zbMATH DE number 1989648 (Why is no real title available?)
| 2003-10-09 | Paper |
scientific article; zbMATH DE number 1954132 (Why is no real title available?)
| 2003-07-28 | Paper |
Display Calculi for Nominal Tense Logics
Journal Of Logic And Computation | 2003-07-25 | Paper |
scientific article; zbMATH DE number 1927419 (Why is no real title available?)
| 2003-06-12 | Paper |
Theoremhood-preserving Maps Characterizing Cut Elimination for Modal Provability Logics
Journal Of Logic And Computation | 2003-03-13 | Paper |
scientific article; zbMATH DE number 1848381 (Why is no real title available?)
| 2003-01-05 | Paper |
Free-variable tableaux for propositional modal logics
Studia Logica | 2002-09-03 | Paper |
Display calculi for logics with relative accessibility relations
Journal of Logic, Language and Information | 2002-07-22 | Paper |
scientific article; zbMATH DE number 1706231 (Why is no real title available?)
| 2002-03-12 | Paper |
Tableau methods for modal and temporal logics
| 2001-11-14 | Paper |
scientific article; zbMATH DE number 1612555 (Why is no real title available?)
| 2001-07-01 | Paper |
Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle
| 2001-05-08 | Paper |
scientific article; zbMATH DE number 1507188 (Why is no real title available?)
| 2001-01-17 | Paper |
scientific article; zbMATH DE number 1341605 (Why is no real title available?)
| 2000-05-11 | Paper |
scientific article; zbMATH DE number 1341474 (Why is no real title available?)
| 2000-02-28 | Paper |
scientific article; zbMATH DE number 1301758 (Why is no real title available?)
| 2000-01-12 | Paper |
scientific article; zbMATH DE number 1301972 (Why is no real title available?)
| 2000-01-12 | Paper |
scientific article; zbMATH DE number 1301971 (Why is no real title available?)
| 1999-12-06 | Paper |
Gaggles, Gentzen and Galois: how to display your favourite substructural logic
Logic Journal of the IGPL | 1999-07-07 | Paper |
Substructural logics on display
Logic Journal of the IGPL | 1998-06-08 | Paper |
Relations between propositional normal modal logics: an overview
Journal Of Logic And Computation | 1998-03-17 | Paper |
scientific article; zbMATH DE number 1086668 (Why is no real title available?)
| 1997-11-13 | Paper |
scientific article; zbMATH DE number 970630 (Why is no real title available?)
| 1997-01-23 | Paper |
scientific article; zbMATH DE number 589742 (Why is no real title available?)
| 1994-11-24 | Paper |
Cut-free sequent and tableau systems for propositional Diodorean modal logics
Studia Logica | 1994-11-10 | Paper |
