Tableau-based reasoning for graph properties
Visualitza/Obre
Lambers.pdf (486,4Kb) (Accés restringit)
Sol·licita una còpia a l'autor
Què és aquest botó?
Aquest botó permet demanar una còpia d'un document restringit a l'autor. Es mostra quan:
- Disposem del correu electrònic de l'autor
- El document té una mida inferior a 20 Mb
- Es tracta d'un document d'accés restringit per decisió de l'autor o d'un document d'accés restringit per política de l'editorial
10.1007/978-3-319-09108-2-2
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/28034
Tipus de documentText en actes de congrés
Data publicació2014
EditorSpringer
Condicions d'accésAccés restringit per política de l'editorial
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
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.
CitacióLambers, L.; Orejas, F. Tableau-based reasoning for graph properties. A: International Conference on Graph Transformations. "Graph Transformation: 7th International Conference, ICGT 2014: held as Part of STAF 2014: York, UK, July 22-24, 2014: proceedings". York: Springer, 2014, p. 17-32.
ISBN978-3-319-09107-5
Versió de l'editorhttp://link.springer.com/chapter/10.1007%2F978-3-319-09108-2_2
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
Lambers.pdf | 486,4Kb | Accés restringit |