Neighbourhood Logic: An Adequate First-order Interval Logic

An interpretation I and an interval [b,e] satisfies dia_l(A) (dia_r(A))
if and only if there exists d greater than equals 0 such that I and
[b-d, e] (or, I and [e, e+d]) satisfy A.

We show the adequacy of NL by deriving the other unary and binary
modalities in a first-order logic in terms of the neighbourhood modalities
and the interval length. We state its axioms and rules and describe the
soundness and completeness results.

We also define various notions of real analysis in terms of dia_l and
dia_r which has opened up the possibility to construct a formal theory
to specify and reason about hybrid systems.

Finally we extend NL to get another Duration Calculus (which will be
called (DC(NL)) and express the liveness and fairness propeties of the
computing system in it.