Tableau-Based Reasoning for Graph Properties (bibtex)
by ,
Abstract:
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 graph properties. A simple way is based on defining an appropriate encoding of graphs in terms of classical logic. This approach has been followed by Courcelle. The alternative is the definition of a specialized logic, as done by Habel and Pennemann, who defined a logic of nested graph conditions, where graph properties are formulated explicitly making use of graphs and graph morphisms, and which has the expressive power of Courcelle̢۪s first order logic of graphs. In particular, in his thesis, Pennemann defined and implemented a sound proof system for reasoning in this logic. Moreover, he showed that his tools outperform some standard provers when working over encoded graph conditions. Unfortunately, Pennemann did not prove the completeness of his proof system. In this sense, one of the main contributions of this paper is the solution to this open problem. In particular, we prove the (refutational) completeness of a tableau method based on Pennemann̢۪s rules that provides a specific theorem-proving procedure for this logic. This procedure can be considered our second contribution. Finally, our tableaux are not standard, but we had to define a new notion of nested tableaux that could be useful for other formalisms where formulas have a hierarchical structure like nested graph conditions.
Reference:
Tableau-Based Reasoning for Graph Properties (Leen Lambers, Fernando Orejas), Chapter in Graph Transformation (Holger Giese, Barbara König, eds.), Springer International Publishing, volume 8571, 2014.
Bibtex Entry:
Powered by bibtexbrowser