In this paper we present two terminating tableau calculi for propositional Dummett logic obeying the subformula property. The ideas of our calculi rely on the linearly ordered Kripke semantics of Dummett logic. The first calculus works on two semantical levels: the present and the next possible world. The second calculus employs the semantical levels of known or not known at the present state of knowledge, that are usual in tableau systems, and exploits a property of the construction of the completeness theorem to introduce a check which is an alternative to loop check mechanisms. © 2013 Springer Science+Business Media Dordrecht.
Fiorino, G. (2014). Terminating Calculi for Propositional Dummett Logic with Subformula Property. JOURNAL OF AUTOMATED REASONING, 52(1), 67-97 [10.1007/s10817-013-9276-7].
Terminating Calculi for Propositional Dummett Logic with Subformula Property
FIORINO, GUIDO GIUSEPPE
2014
Abstract
In this paper we present two terminating tableau calculi for propositional Dummett logic obeying the subformula property. The ideas of our calculi rely on the linearly ordered Kripke semantics of Dummett logic. The first calculus works on two semantical levels: the present and the next possible world. The second calculus employs the semantical levels of known or not known at the present state of knowledge, that are usual in tableau systems, and exploits a property of the construction of the completeness theorem to introduce a check which is an alternative to loop check mechanisms. © 2013 Springer Science+Business Media Dordrecht.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.