| || || |
| || |
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 ﬁrst-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 conﬂuence.
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 ﬁle contains instructions how to use Prover9 for proving PITL theorems.
| || |