AAAI Publications, Twenty-Second International Joint Conference on Artificial Intelligence

Font Size: 
Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World
Guido Fiorino

Last modified: 2011-06-28


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.

Full Text: PDF