8 Conclusion and future work

Conclusion and future work [Slide 28]

• An interval temporal algebraic encoding of PITL in Prover9 results in quite a useful tool
• need to reduce the axioms of ITA
• replace some of the more complex axioms of ITA by simpler ones,
• Use a different ATP
• Integration of Description Logic axiom system with Interval Temporal Algebra axiom system