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 Citations (Scopus)

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.

Automated reasoning for the dialetheic logic RM3. / Pelletier, Francis Jeffry; Sutcliffe, Geoffrey; Hazen, Allen P.

FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference. AAAI Press, 2017. p. 110-115.

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

Pelletier, FJ, Sutcliffe, G & Hazen, AP 2017, Automated reasoning for the dialetheic logic RM3. in FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference. AAAI Press, pp. 110-115, 30th International Florida Artificial Intelligence Research Society Conference, FLAIRS 2017, Marco Island, United States, 5/22/17.
Pelletier FJ, Sutcliffe G, Hazen AP. Automated reasoning for the dialetheic logic RM3. In FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference. AAAI Press. 2017. p. 110-115
Pelletier, Francis Jeffry ; Sutcliffe, Geoffrey ; Hazen, Allen P. / Automated reasoning for the dialetheic logic RM3. FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference. AAAI Press, 2017. pp. 110-115
@inproceedings{26a19b84e56b4679add57e9911999f26,
title = "Automated reasoning for the dialetheic logic RM3",
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.",
author = "Pelletier, {Francis Jeffry} and Geoffrey Sutcliffe and Hazen, {Allen P.}",
year = "2017",
language = "English (US)",
pages = "110--115",
booktitle = "FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference",
publisher = "AAAI Press",

}

TY - GEN

T1 - Automated reasoning for the dialetheic logic RM3

AU - Pelletier, Francis Jeffry

AU - Sutcliffe, Geoffrey

AU - Hazen, Allen P.

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85029545304&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85029545304&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:85029545304

SP - 110

EP - 115

BT - FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference

PB - AAAI Press

ER -