Automated reasoning for the dialetheic logic RM3

Francis Jeffry Pelletier, Geoffrey Sutcliffe, Allen P. Hazen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

This paper describes a system for automated reasoning in the dialetheic logic RM3. A dialetheic logic allows formulae to be true, or false, or (differently from classical logic) both true and false, and the connectives are interpreted in terms of these three truth values. Consequently some inference rules of classical logic are invalid in RM3, and some theorems of classical logic are not theorems of RM3. An automated theorem prover for first-order RM3 has been developed, based on translations of RM3 formulae to classical first-order logic, and use of existing first-order reasoning systems to reason over the translated formulae. Examples and results are provided to highlight the differences between reasoning in RM3 and classical logic.

Original languageEnglish (US)
Title of host publicationFLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference
PublisherAAAI Press
Pages110-115
Number of pages6
ISBN (Electronic)9781577357872
StatePublished - 2017
Event30th International Florida Artificial Intelligence Research Society Conference, FLAIRS 2017 - Marco Island, United States
Duration: May 22 2017May 24 2017

Other

Other30th International Florida Artificial Intelligence Research Society Conference, FLAIRS 2017
CountryUnited States
CityMarco Island
Period5/22/175/24/17

ASJC Scopus subject areas

  • Artificial Intelligence
  • Software

Cite this

Pelletier, F. J., Sutcliffe, G., & Hazen, A. P. (2017). Automated reasoning for the dialetheic logic RM3. In FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference (pp. 110-115). AAAI Press.