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.
Articolo in rivista - Articolo scientifico
Dummett logic, Tableau calculi, Automated theorem proving, Subformula property
English
2014
52
1
67
97
none
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].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/43313
Citazioni
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
Social impact