On the Priorean temporal logic with [d] over the real line.

We consider the language with temporal operators G, H and coderivative operator [d]. G means 'always in the future', H means 'always in the past' and [d] means 'around now but possibly not now'. We finitely axiomatize the logic of this language interpreted over the real line, we prove that this logic is PSPACE-complete, and that it is neither strongly complete nor Kripke-complete (and consequently that it fails the finite model property). [ABSTRACT FROM AUTHOR]