4.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

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

Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024