An adequate first order interval logic

Abstract

This paper introduces left and right neighbourhoods as primitive interval modalities to define other unary and binary modalities of intervals in a first order logic with interval length. A complete first order logic for the neighbourhood modalities is presented. It is demonstrated how the logic can support formal specification and verification of liveness and fairness, and also of various notions of real analysis.