Automated Reasoning for the Dialetheic Logic RM3
Abstract
This talk 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 RM3 has been developed, based on translations
of RM3 formulae to classical first-order logic, and use of an existing
first-order theorem prover to reason over the translated formulae.
Examples and results are provided to highlight the differences
between reasoning in classical logic and in RM3.