© 1996-2021

3.4 ITL Theorem Prover based on Prover9

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

  • Version 1.5 (first public release: 05/12/2008): gzipped tar file.

The README in this tar file contains instructions how to use Prover9 for proving PITL theorems.

Contact | Home | ITL home | Course | Proofs | Algebra | FL