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:

Rationale [Slide 3]

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:

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