Journal of Logic and Computation, Volume 10, Issue 2, pp. 271-295: Abstract.
Completeness of neighbourhood logic
R Barua1, S Roy2 and Z Chaochen3
1Division of Theoretical Statistics and Mathematics, Indian Statistical Institute, 203 B.T. Road, Calcutta, 700 035, India, E-mail: email@example.com, 2Department of Computer Science and Automation, Indian Institute of Science, Bangalore 560 012, India, E-mail: firstname.lastname@example.org, 3International Institute for Software Technology, United Nations University, UNU/IIST, PO Box 3057, Macau, E-mail: email@example.com
This paper presents a completeness result for a first-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 can 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.
Keywords: modal logic, neighbourhood modalities, first-order interval logic, completeness, interval models, Kripke models.