×

Relational dual tableau decision procedures and their applications to modal and intuitionistic logics. (English) Zbl 1317.03017

Authors’ abstract: We study a class \(\mathcal{DL}\) of certain decidable relational logics of binary relations with a single relational constant and restricted composition. The logics in \(\mathcal{DL}\) are defined in terms of semantic restrictions on the models. The main contribution of the present article is the construction of relational dual tableau decision procedures for the logics in \(\mathcal{DL}\). The systems are constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. All necessary bookkeeping is contained in the proof tree itself and used according to the explicit rules. All the systems are deterministic, producing exactly one proof tree for every formula. Furthermore, we show how the systems for logics in \(\mathcal{DL}\) can be used as deterministic decision procedures for some modal and intuitionistic logics.
Reviewer: Nail Zamov (Kazan)

MSC:

03B25 Decidability of theories and sets of sentences
03F03 Proof theory in general (including proof-theoretic semantics)
03B45 Modal logic (including the logic of norms)
03B20 Subsystems of classical logic (including intuitionistic logic)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bresolin, D.; Golińska-Pilarek, J.; Orłowska, E., Relational dual tableaux for interval temporal logics, J. Appl. Non-Classical Logics, 16, 3-4, 251-277 (2006) · Zbl 1186.03035
[2] Burrieza, A.; Ojeda-Aciego, M.; Orłowska, E., Relational approach to order-of-magnitude reasoning, Lecture Notes in Comput. Sci., 4342, 105-124 (2006) · Zbl 1177.68178
[3] Cantone, D.; Asmundo, M. N.; Orłowska, E., Dual tableau-based decision procedures for relational logics with restricted composition operator, J. Appl. Non-Classical Logics, 21, 2, 177-200 (2011) · Zbl 1242.03028
[4] Formisano, A.; Nicolosi-Asmundo, M., An efficient relational deductive system for propositional non-classical logics, J. Appl. Non-Classical Logics, 16, 3-4, 367-408 (2006) · Zbl 1186.03044
[5] Glivenko, V., Sur quelques points de la logique de M. Brouwer, Bull. Cl. Sci., 5, 15, 183-188 (1929) · JFM 55.0030.05
[6] Golińska-Pilarek, J.; Muñoz-Velasco, E., Relational approach for a logic for order of magnitude qualitative reasoning with negligibility, non-closeness and distance, Log. J. IGPL, 17, 4, 375-394 (2009) · Zbl 1171.68043
[7] Golińska-Pilarek, J.; Muñoz-Velasco, E., Reasoning with qualitative velocity: towards a hybrid approach, Lecture Notes in Comput. Sci., 7208, 635-646 (2012)
[8] Golińska-Pilarek, J.; Orłowska, E., Tableaux and dual tableaux: transformation of proofs, Studia Logica, 85, 291-310 (2007) · Zbl 1125.03041
[9] Golińska-Pilarek, J.; Orłowska, E., Dual tableau for monoidal triangular norm logic \(MTL\), Fuzzy Sets and Systems, 162, 1, 39-52 (2011) · Zbl 1216.03045
[10] Golińska-Pilarek, J.; Muñoz-Velasco, E.; Mora, A., A new deduction system for deciding validity in modal logic \(K\), Log. J. IGPL, 19, 2, 425-434 (2011) · Zbl 1252.03027
[11] Golińska-Pilarek, J.; Muñoz-Velasco, E.; Mora-Bonilla, A., Relational dual tableau decision procedure for modal logic \(K\), Log. J. IGPL, 20, 4, 747-756 (2012) · Zbl 1264.03041
[12] Konikowska, B., Rasiowa-Sikorski deduction systems in computer science applications, Theoret. Comput. Sci., 286, 2, 323-366 (2002) · Zbl 1058.03029
[13] Konikowska, B., A decompositional deduction system for a logic featuring inconsistency and uncertainty, J. Appl. Non-Classical Logics, 15, 1, 25-44 (2005) · Zbl 1185.03048
[14] Monk, D., On representable relation algebras, Michigan Math. J., 11, 3, 207-210 (1964) · Zbl 0137.00603
[15] Mora, A.; Muñoz-Velasco, E.; Golińska-Pilarek, J., Implementing a relational theorem prover for modal logic \(K\), Int. J. Comput. Math., 88, 9, 1869-1884 (2011) · Zbl 1229.03019
[16] Orłowska, E., Relational interpretation of modal logics, (Andréka, H.; Monk, D.; Németi, I., Algebraic Logic. Algebraic Logic, Colloq. Math. Soc. János Bolyai, vol. 54 (1988), North-Holland: North-Holland Amsterdam), 443-471 · Zbl 0751.03009
[17] Orłowska, E.; Golińska-Pilarek, J., Dual Tableaux: Foundations, Methodology, Case Studies (2011), Springer · Zbl 1210.03001
[18] Rasiowa, H.; Sikorski, R., On Gentzen theorem, Fund. Math., 48, 57-69 (1960) · Zbl 0099.00603
[19] Rasiowa, H.; Sikorski, R., The Mathematics of Metamathematics (1963), Polish Scientific Publishers: Polish Scientific Publishers Warsaw · Zbl 0122.24311
[20] Tarski, A., On the calculus of relations, J. Symbolic Logic, 6, 73-89 (1941) · JFM 67.0973.02
[21] Tarski, A.; Givant, S. R., A Formalization of Set Theory Without Variables (1987), Amer. Math. Soc. · Zbl 0654.03036
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.