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.
Fiorino, G. (2011). Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (pp.869-874). AAAI Press [10.5591/978-1-57735-516-8/IJCAI11-151].
Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World
FIORINO, GUIDO GIUSEPPE
2011
Abstract
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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
