Complteness of Neighbourhood Logic

摘要

This paper presents a completeness result for a fist-order interval temporal logic, called Neighbourhood Logic (NL) which has two neighbourhood modalities. NL can support the specification of liveness and fairness properties of computing systems as well as formalization of many concepts of real analysis. The two neighbourhood modalities are also adequate in the sense that they ca derive other important unary and binary modalities of interval temporal logic. We prove the completeness result for NL by giving a Kripke model semantics and then mapping the Kripke models to the interval models for NL.