### 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 language | English (US) |
---|---|

Title of host publication | FLAIRS 2017 - Proceedings of the 30th International Florida Artificial Intelligence Research Society Conference |

Publisher | AAAI Press |

Pages | 110-115 |

Number of pages | 6 |

ISBN (Electronic) | 9781577357872 |

State | Published - 2017 |

Event | 30th International Florida Artificial Intelligence Research Society Conference, FLAIRS 2017 - Marco Island, United States Duration: May 22 2017 → May 24 2017 |

### Other

Other | 30th International Florida Artificial Intelligence Research Society Conference, FLAIRS 2017 |
---|---|

Country | United States |

City | Marco Island |

Period | 5/22/17 → 5/24/17 |

### ASJC Scopus subject areas

- Artificial Intelligence
- Software

### Cite this

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

}

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 -