Fernando Orejas, Universitat Politecnica de Catalunya
A logic for reasoning about graphs
Note: Fernando is on a long-term visit to RHUL.
Graphs are ubiquitous in Computer Science. For this reason, in many areas, it is very important to have the means to express and reason about the properties that a given graph may or may not satisfy. In particular, our work is motivated by model-driven software development and by graph data bases. With this aim, in this seminar I will present a visual logic that allow us to describe graph properties, including properties about paths, which has the expressive power of first-order logic, if we do not consider path properties. The logic is equipped with a deductive tableau method that we have proved to be sound and complete. Moreover, we have shown that this logic is an institution.