A Note on Gödel-Dummet Logic LC

Let \(A_{0},A_{1},...,A_{n}\) be (possibly) distintict wffs, \(n\) being an odd number equal to or greater than 1. Intuitionistic Propositional Logic IPC plus the axiom \((A_{0}\rightarrow A_{1})\vee ...\vee (A_{n-1}\rightarrow A_{n})\vee (A_{n}\rightarrow A_{0})\) is equivalent to Gödel-Dummett logic LC. However, if \(n\) is an even number equal to or greater than 2, IPC plus the said axiom is a sublogic of LC.

Tableau Calculus for Dummett Logic Based on Present and Next State of Knowledge

In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly increasing the number of forced propositional variables after the application of non-invertible rules. The focus of the paper is on a new tableau system for Dummett logic, for which we have an implementation. The ideas presented can be extended to intuitionistic logic and intermediate logics as well.

Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus

We present a procedure to decide propositional Dummett logic. Such a procedure relies on a tableau calculus with a multiple premise rule and optimizations. The resulting implementation outperforms the state of the art graph-based procedure.