Mark Reynolds

Tableau for temporal logic over general linear time

We use mosaics (and games) to provide a simple, sound and complete tableau reasoning procedure for the temporal logic of until and since over general linear time.