Abstract
The tautology problem is the problem to prove the validity of statements. In this paper, we present a calculus for this undecidable problem on graphical conditions, prove its soundness, investigate the necessity of each deduction rule, and discuss practical aspects concerning an implementation. As we use the framework of weak adhesive HLR categories, the calculus is applicable to a number of replacement capable structures, such as Petri-Nets, graphs or hypergraphs.
This work is supported by the German Research Foundation (DFG), grants GRK 1076/1 (Graduate School on Trustworthy Software Systems) and HA 2936/2 (Development of Correct Graph Transformation Systems).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. Journal on Artificial Intelligence Tools 15(1), 21–52 (2006)
Courcelle, B.: Graph rewriting: An algebraic and logical approach. In: Handbook of Theoretical Computer Science, vol. B, pp. 193–242. Elsevier, Amsterdam (1990)
Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1989)
Ehrig, H., Ehrig, K., Habel, A., Pennemann, K.-H.: Theory of constraints and application conditions: From graphs to high-level structures. Fundamenta Informaticae 74, 135–166 (2006)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. EATCS Monographs of Theoretical Computer Science. Springer, Berlin (2006)
Habel, A., Plump, D.: Computational completeness of programming languages based on graph transformation. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 230–245. Springer, Heidelberg (2001)
Habel, A., Pennemann, K.-H.: Nested constraints and application conditions for high-level structures. In: Kreowski, H.-J., Montanari, U., Orejas, F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems Modeling. LNCS, vol. 3393, pp. 293–308. Springer, Heidelberg (2005)
Habel, A., Pennemann, K.-H.: Correctness of high-level transformation systems relative to nested conditions. In: MSCS 2008 (Accepted for publication, 2008)
Habel, A., Pennemann, K.-H., Rensink, A.: Weakest preconditions for high-level programs. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 445–460. Springer, Heidelberg (2006)
Heckel, R., Wagner, A.: Ensuring consistency of conditional graph grammars. In: SEGRAGRA 1995. ENTCS, vol. 2, pp. 95–104 (1995)
Koch, M., Mancini, L.V., Parisi-Presicce, F.: Graph-based specification of access control policies. JCSS 71, 1–33 (2005)
McCune, W.: Homepage of Prover9 (2008), http://www.prover9.org/
Orejas, F., Ehrig, H., Prange, U.: A logic of graph constraints. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 179–199. Springer, Heidelberg (2008)
Orejas, F.: Attributed graph constraints. In: Ehrig, H., et al. (eds.) Proc. ICGT 2008. LNCS, vol. 5214, Springer, Heidelberg (2008)
Pennemann, K.-H.: Generalized constraints and application conditions for graph transformation systems. Master’s thesis, Department of Computing Science, University of Oldenburg, Oldenburg (2004)
Pennemann, K.-H.: An algorithm for approximating the satisfiability problem of high-level conditions. In: Proc. GT-VC 2007. ENTCS, vol. 213, pp. 75–94. Elsevier, Amsterdam (2008)
Rensink, A.: Representing first-order logic by graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 319–335. Springer, Heidelberg (2004)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12, 23–41 (1965)
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(2-3), 91–110 (2002)
Strecker, M.: Modeling and verifying graph transformations in proof assistants. In: Proc. Termgraph 2007. ENTCS, vol. 203, pp. 135–148. Elsevier, Amsterdam (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pennemann, KH. (2008). Resolution-Like Theorem Proving for High-Level Conditions. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds) Graph Transformations. ICGT 2008. Lecture Notes in Computer Science, vol 5214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87405-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-87405-8_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87404-1
Online ISBN: 978-3-540-87405-8
eBook Packages: Computer ScienceComputer Science (R0)