Automated Reasoning for the Dialetheic Logic RM3

Background and Motivation

• Automated Reasoning
• Classical First-order Logic
• Dialetheic Logic
• The Logic RM3

Automated Reasoning for RM3

• Indirect Proofs
• The Translational Approach
• The Truth Evaluation Approach
• The Implementation

Examples and Evaluation

• Simple Examples
• A Set Theory Paradox (or not)
• Evaluation on the TPTP

Conclusion

The End - Any Questions?