Conclusion

Strengths and Weaknesses

• A new technique for reasoning in the event calculus

• Provides humanly-readable proofs
• Weaker than SAT approach
• Limited arithmetic

• Provides new problems for the TPTP

Future

• Improved RDN axiomatization of arithmetic
• Use of built-in arithmetic

• Extension to non-discrete event calculus