Decidable Navigation Logics for Object Structures

In this paper, we introduce decidable multimodal logics to describe and reason about navigation across object structures. The starting point of these navigation logics is the modelling of object structures as Kripke models that contain a family of deterministic accessibility relations; one for each pointer attribute. These pointer attributes are used in the logics both as first-order terms in equalities and as modal operators. To handle the ambiguities of pointer attributes the logics also cover a mechanism to bind logical variables to objects that are reachable by a pointer. The main result of this paper is a tableau construction for deciding the validity of formulas in the navigation logics.

• Type: Conference
• Year: 2001
• Where: CSL
• Authors: Frank S. de Boer, Rogier M. van Eijk
• Keywords: Automated Reasoning, CSL 2001, Logics, Navigation Logics, Pointer Attributes