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.

Comment: 32 pages

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

Source: arXiv.org:1104.4131

Volume: Volume 7, Issue 2

Secondary volumes: Selected Papers of the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009)

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, 2022, SAT-Based Proof Search in Intermediate Propositional Logics, Lecture notes in computer science, pp. 57-74, 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, 2021, Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity, Lecture notes in computer science, pp. 41-57, 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, 2019, From Simplified Kripke-Style Semantics to Simplified Analytic Tableaux for Some Normal Modal Logics, Lecture notes in computer science, pp. 116-131, 10.1007/978-3-030-35166-3_9.

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

Roy Dyckhoff, 2016, Intuitionistic Decision Procedures Since Gentzen, Progress in computer science and applied logic, pp. 245-267, 10.1007/978-3-319-29198-7_6.

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, 2015, Modal Tableau Systems with Blocking and Congruence Closure, Lecture notes in computer science, pp. 38-53, 10.1007/978-3-319-24312-2_4.

John G. Stell;Renate A. Schmidt;David Rydeheard, 2014, Tableau Development for a Bi-intuitionistic Tense Logic, Lecture notes in computer science, pp. 412-428, 10.1007/978-3-319-06251-8_25.

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, 2013, A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal{SHOI}$, Lecture notes in computer science, pp. 188-202, 10.1007/978-3-642-40537-2_17.

Clare Dixon;Boris Konev;Renate A. Schmidt;Dmitry Tishkovsky, 2012, Labelled Tableaux for Temporal Logic with Cardinality Constraints, Research Explorer (The University of Manchester), 1397, pp. 111-118, 10.1109/synasc.2012.47.

Deepak Garg;Valerio Genovese;Sara Negri, 2012, Countermodels from Sequent Calculi in Multi-Modal Logics, CINECA IRIS Institutial Research Information System (University of Genoa), pp. 315-324, 10.1109/lics.2012.42.

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

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3897 times.

This article's PDF has been downloaded 1055 times.