Note: this work has been re-encoded in the deep embedding of propositional ITL in Isabelle/HOL.
Prover9 is a resolution/paramodulation automated theorem prover for first-order and equational logic developed by William McCune.
We have given an algebraic axiom system for Propositional Interval Temporal Logic (PITL): Interval Temporal Algebra. The axiom system is a combination of a variant of Kleene algebra and Omega algebra plus axioms for linearity and confluence.
This algebraic axiom system for PITL has been encoded in Prover9. So we can use Prover9 to prove the validity of various PITL theorems. The Prover9 encoding of PITL plus examples of more than 300 PITL theorems are available for download as
Version 1.8 (released 27/08/2009): gzipped tar file.
- documentation updated to new semantics for chopstar and chop omega algebraic operators
Version 1.7 (released 15/05/2009): gzipped tar file.
- updated documentation in doc, to use new ITL semantics
Version 1.6 (released 12/12/2008): gzipped tar file.
- changed copyright license to GPLv3.0 and added the notice to all files
The README in this tar file contains instructions how to use Prover9 for proving PITL theorems.