Automated Proof Support for Interval Logics

We outline the background and motivation for the use of interval logics and consider some initial attempts toward proof support and automation. The main focus, though, is on recent work on these subjects. We compare different proof theoretical formalisms, in particular a “classical” versus a “labelled” one.

We discuss encodings of these in the generic proof assistant Isabelle and consider some examples which show that in some cases the labelled formalism gives an order of magnitude improvement in proof length compared to a classical approach.