Conclusion

Contributions

• New theory translating RM3 to FOL
• First automated reasoning system for RM3 (TTBOOK)
• Revelation of some interesting non-theorems

Future Work

• Study interesting FOL theorems, not RM3 theorems
• Translate equality
• Extend to FDE logic
• Applications