Automated Synthesis of Tableau Calculi

Renate A. Schmidt; Dmitry Tishkovsky

doi:10.2168/LMCS-7(2:6)2011

Renate A. Schmidt ; Dmitry Tishkovsky - Automated Synthesis of Tableau Calculi

lmcs:970 - Logical Methods in Computer Science, May 7, 2011, Volume 7, Issue 2 - https://doi.org/10.2168/LMCS-7(2:6)2011

Automated Synthesis of Tableau CalculiArticle

Authors: Renate A. Schmidt ; Dmitry Tishkovsky

This paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau inference rules that can then be used to reason within the logic. The method guarantees that the generated rules form a calculus which is sound and constructively complete. If the logic can be shown to admit finite filtration with respect to a well-defined first-order semantics then adding a general blocking mechanism provides a terminating tableau calculus. The process of generating tableau rules can be completely automated and produces, together with the blocking mechanism, an automated procedure for generating tableau decision procedures. For illustration we show the workability of the approach for a description logic with transitive roles and propositional intuitionistic logic.

https://doi.org/10.2168/LMCS-7(2:6)2011

Source: arXiv.org:1104.4131

Volume: Volume 7, Issue 2

Published on: May 7, 2011

Imported on: May 29, 2010

Keywords: Computer Science - Logic in Computer Science,Computer Science - Symbolic Computation,cs.SC

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

03B35 - Mechanization of proofs and logical operations

Sources:

[1] zbMATH Open.

Bibliographic References

14 Documents citing this article

Camillo Fiorentini;Mauro Ferrari, Lecture notes in computer science, SAT-Based Proof Search in Intermediate Propositional Logics, pp. 57-74, 2022, 10.1007/978-3-031-10769-6_5, https://doi.org/10.1007/978-3-031-10769-6_5.

Joanna Golińska-Pilarek;Taneli Huuskonen;Michał Zawidzki, Lecture notes in computer science, Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity, pp. 41-57, 2021, 10.1007/978-3-030-79876-5_3, https://doi.org/10.1007/978-3-030-79876-5_3.

Peter Baumgartner;Renate A. Schmidt, 2019, Blocking and Other Enhancements for Bottom-Up Model Generation Methods, Journal of Automated Reasoning, 64, 2, pp. 197-251, 10.1007/s10817-019-09515-1, https://doi.org/10.1007/s10817-019-09515-1.

Yaroslav Petrukhin;Michał Zawidzki, Lecture notes in computer science, From Simplified Kripke-Style Semantics to Simplified Analytic Tableaux for Some Normal Modal Logics, pp. 116-131, 2019, 10.1007/978-3-030-35166-3_9.

Yoni Zohar;Dmitry Tishkovsky;Renate A. Schmidt;Anna Zamansky, Lecture notes in computer science, Automating Automated Reasoning, pp. 610-638, 2019, 10.1007/978-3-030-22102-7_29.

Roy Dyckhoff, St Andrews Research Repository (St Andrews Research Repository), Intuitionistic Decision Procedures Since Gentzen, pp. 245-267, 2016, 10.1007/978-3-319-29198-7_6, http://hdl.handle.net/10023/8824.

John G. Stell;Renate A. Schmidt;David Rydeheard, 2015, A bi-intuitionistic modal logic: Foundations and automation, Journal of Logical and Algebraic Methods in Programming, 85, 4, pp. 500-519, 10.1016/j.jlamp.2015.11.003, https://doi.org/10.1016/j.jlamp.2015.11.003.

Renate A. Schmidt;Uwe Waldmann, Research Explorer (The University of Manchester), Modal Tableau Systems with Blocking and Congruence Closure, pp. 38-53, 2015, 10.1007/978-3-319-24312-2_4, https://pure.manchester.ac.uk/ws/files/32297317/FULL_TEXT.PDF.

John G. Stell;Renate A. Schmidt;David Rydeheard, White Rose Research Online (University of Leeds), Tableau Development for a Bi-intuitionistic Tense Logic, pp. 412-428, 2014, 10.1007/978-3-319-06251-8_25, http://eprints.whiterose.ac.uk/78797/8/paper_14%20%281%29_with_coversheet.pdf.

Renate A. Schmidt;Dmitry Tishkovsky, 2014, Using tableau to decide description logics with full role negation and identity, ACM Transactions on Computational Logic, 15, 1, pp. 1-31, 10.1145/2559947, https://doi.org/10.1145/2559947.

Mohammad Khodadadi;Renate A. Schmidt;Dmitry Tishkovsky, Lecture notes in computer science, A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$, pp. 188-202, 2013, 10.1007/978-3-642-40537-2_17.

Clare Dixon;Boris Konev;Renate A. Schmidt;Dmitry Tishkovsky, CiteSeer X (The Pennsylvania State University), Labelled Tableaux for Temporal Logic with Cardinality Constraints, pp. 111-118, 2012, Timisoara, Romania, 10.1109/synasc.2012.47, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.592.2459.

Deepak Garg;Valerio Genovese;Sara Negri, 2012 27th Annual IEEE Symposium on Logic in Computer Science, Countermodels from Sequent Calculi in Multi-Modal Logics, pp. 315-324, 2012, Dubrovnik, Croatia, 10.1109/lics.2012.42.

Renate A. Schmidt, Lecture notes in computer science, Synthesising Terminating Tableau Calculi for Relational Logics, pp. 40-49, 2011, 10.1007/978-3-642-21070-9_3.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1988 times.

This article's PDF has been downloaded 705 times.