2 Rationale

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 logic operators.

• ITL Library for PVS. Antonio Cau (1997).

  Interactive theorem prover for (in)finite first order ITL, requires expert proof knowledge and has little automation.

• DCVALID. Paritosh Pandya (2000).

  Quantified 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 complexity.

Rationale [Slide 3]

• PITL2Mona. Rodolfo Gomez (2004).

  Translate finite Propositional ITL (PITL) into WS1S, use decision procedure of WS1S (MONA). WS1S has non-elementary complexity.

• FL2CUDD. Ben Moszkowski (2005).

  Use a subset of (in)finite 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 off-the-shelf automated proof and counterexample search tools (ATP) for first-order and equational logic.

Rationale [Slide 4]

Inspired by the work of Peter Höffner, 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 off-the shelf ATP Prover9 (first-order and equational logic, William McCune).