7 Automatic theorem prover for PITL

Automatic theorem prover for PITL [Slide 27]

• Take an off-the-shelf automatic theorem prover (ATP)
• encode the algebraic rules for an interval temporal algebra within it

We used Prover9 as ATP and encoded the interval temporal algebraic rules.

• Proved more than 350 PITL theorems so far
• Derived all PITL axioms/proof rules from ITA’s axioms

Demo