### 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)ﬁ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 complexity.

#### Rationale [Slide 3]

• PITL2Mona. Rodolfo Gomez (2004).

Translate ﬁnite 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)ﬁ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).

 2018-02-26 Contact | Home | ITL home | Course | Proofs | Algebra | FL