TY  - JOUR
A1  - Navarro, Marisa
A1  - Orejas, Fernando
A1  - Pino, Elvira
A1  - Lambers, Leen
T1  - A navigational logic for reasoning about graph properties
JF  - Journal of logical and algebraic methods in programming
N2  - Graphs play an important role in many areas of Computer Science. In particular, our work is motivated by model-driven software development and by graph databases. For this reason, it is very important to have the means to express and to reason about the properties that a given graph may satisfy. With this aim, in this paper we present a visual logic that allows us to describe graph properties, including navigational properties, i.e., properties about the paths in a graph. The logic is equipped with a deductive tableau method that we have proved to be sound and complete.
KW  - Graph logic
KW  - Algebraic methods
KW  - Formal modelling
KW  - Specification
Y1  - 2021
U6  - https://doi.org/10.1016/j.jlamp.2020.100616
SN  - 2352-2208
SN  - 2352-2216
VL  - 118
PB  - Elsevier Science
CY  - Amsterdam [u.a.]
ER  - 
TY  - JOUR
A1  - Orejas, Fernando
A1  - Pino, Elvira
A1  - Navarro, Marisa
A1  - Lambers, Leen
T1  - Institutions for navigational logics for graphical structures
JF  - Theoretical computer science
N2  - We show that a Navigational Logic, i.e., a logic to express properties about graphs and about paths in graphs is a semi-exact institution. In this way, we can use a number of operations to structure and modularize our specifications. Moreover, using the properties of our institution, we also show how to structure single formulas, which in our formalism could be quite complex.
KW  - Institutions
KW  - Graph logics
KW  - Navigational logics
Y1  - 2018
U6  - https://doi.org/10.1016/j.tcs.2018.02.031
SN  - 0304-3975
SN  - 1879-2294
VL  - 741
SP  - 19
EP  - 24
PB  - Elsevier
CY  - Amsterdam
ER  -