| || |
Rationale [Slide 2]
An Automated Theorem Prover (ATP) for Interval Temporal Logic (ITL)
has always been a desirable tool. There have been various attempts to
implement such ATPs:
- Lite. Shinji Kono (1991 (Prolog), 2008 (Java)).
Tableau-based, exponential in the number of the variables in the
formula and also combinatorial w.r.t. to the nesting of temporal
- ITL Library for PVS. Antonio Cau (1997).
Interactive theorem prover for (in)ﬁnite ﬁrst order ITL, requires
expert proof knowledge and has little automation.
- DCVALID. Paritosh Pandya (2000).
Quantiﬁed Discrete time Duration Calculus (QDDC). Translate
QDDC into WS1S, use decision procedure of WS1S (MONA,
Nils Klarlund and Anders Møller). WS1S has non-elementary
Rationale [Slide 3]
- PITL2Mona. Rodolfo Gomez (2004).
Translate ﬁnite Propositional ITL (PITL) into WS1S, use
decision procedure of WS1S (MONA). WS1S has non-elementary
- FL2CUDD. Ben Moszkowski (2005).
Use a subset of (in)ﬁnite PITL called Fusion Logic (FL). The
decision procedure of FL is built on top of Colorado University
Decision Diagram (CUDD, Fabio Somenzi).
So mainly modelchecking or special purpose automated deduction.
There are oﬀ-the-shelf automated proof and counterexample search
tools (ATP) for ﬁrst-order and equational logic.
Rationale [Slide 4]
Inspired by the work of Peter Höﬀner, Georg Struth and Bernhard
Möller we proceed as follows:
- Introduce Interval Temporal Algebra (ITA). An ITA is based on
Kleene Algebra and Omega Algebra.
- Show that PITL is an ITA.
- Encode the axiom system for ITA in an oﬀ-the shelf ATP Prover9
(ﬁrst-order and equational logic, William McCune).