Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World

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.

Cite

Text

Fiorino. "Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World." International Joint Conference on Artificial Intelligence, 2011. doi:10.5591/978-1-57735-516-8/IJCAI11-151

Markdown

[Fiorino. "Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World." International Joint Conference on Artificial Intelligence, 2011.](https://mlanthology.org/ijcai/2011/fiorino2011ijcai-refutation/) doi:10.5591/978-1-57735-516-8/IJCAI11-151

BibTeX

@inproceedings{fiorino2011ijcai-refutation,
  title     = {{Refutation in Dummett Logic Using a Sign to Express the Truth at the Next Possible World}},
  author    = {Fiorino, Guido},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2011},
  pages     = {869-874},
  doi       = {10.5591/978-1-57735-516-8/IJCAI11-151},
  url       = {https://mlanthology.org/ijcai/2011/fiorino2011ijcai-refutation/}
}