{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:52:39Z","timestamp":1762458759408},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2010,5,1]],"date-time":"2010-05-01T00:00:00Z","timestamp":1272672000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2010,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Graph constraints were introduced in the area of graph transformation, in connection with the notion of (negative) application conditions, as a form to limit the applicability of transformation rules. However, we believe that graph constraints may also play a significant role in the area of visual software modelling or in the specification and verification of semi-structured documents or websites (i.e. HTML or XML sets of documents). In this sense, after some discussion on these application areas, we concentrate on the problem of how to prove the consistency of specifications based on this kind of constraints. In particular, we present proof rules for two classes of graph constraints and show that our proof rules are sound and (refutationally) complete for each class. In addition, we study clause subsumption in this context as a form to speed up refutation.<\/jats:p>","DOI":"10.1007\/s00165-009-0116-9","type":"journal-article","created":{"date-parts":[[2009,7,3]],"date-time":"2009-07-03T12:49:37Z","timestamp":1246625377000},"page":"385-422","source":"Crossref","is-referenced-by-count":12,"title":["Reasoning with graph constraints"],"prefix":"10.1145","volume":"22","author":[{"given":"Fernando","family":"Orejas","sequence":"first","affiliation":[{"name":"Dpto de L.S.I., Universitat Polit\u00e8cnica de Catalunya, Campus Nord, M\u00f2dul Omega, Jordi Girona 1-3, 08034, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hartmut","family":"Ehrig","sequence":"additional","affiliation":[{"name":"Fak. IV, Technische Universit\u00e4t Berlin, Franklinstrasse 28\/29, 10587, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrike","family":"Prange","sequence":"additional","affiliation":[{"name":"Fak. IV, Technische Universit\u00e4t Berlin, Franklinstrasse 28\/29, 10587, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Taentzer G (2004) AGG: a graph transformation environment for modeling and validation of software. In: Pfaltz J Nagl M Boehlen B (eds) Application of graph transformations with industrial relevance (AGTIVE903) LNCS 3062. Springer Heidelberg pp 446\u2013456. URL:http:\/\/tfs.cs.tu-berlin.de\/agg","DOI":"10.1007\/978-3-540-25959-6_35"},{"key":"e_1_2_1_2_2_2","first-page":"565","article-title":"Automated verification of web sites using partial rewriting","volume":"8","author":"Alpuente M","year":"2006","journal-title":"Softw Tools Technol Transf"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Baldan P Corradini A Koenig B Lluch-Lafuente A (2007) A temporal graph logic for verification of graph transformation systems. In: Recent trends in algebraic development techniques 18th international workshop WADT 2006. Springer Lecture Notes in Computer Science vol 4409 pp 1\u201320","DOI":"10.1007\/978-3-540-71998-4_1"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Courcelle B (1997) The expression of graph properties and graph transformations in monadic second-order logic in [Roz97] pp 313\u2013400","DOI":"10.1142\/9789812384720_0005"},{"key":"e_1_2_1_2_5_2","volume-title":"Fundamentals of algebraic graph transformation","author":"Ehrig H","year":"2006"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Ehrig E Ehrig K Habel A Pennemann KH (2004) Constraints and application conditions: from graphs to high-level structures. In: Ehrig H Engels G Parisi-Presicce F Rozenberg G (eds) Graph transformations second international conference ICGT 2004. Springer Lecture Notes in Computer Science vol 3256 pp 287\u2013303","DOI":"10.1007\/978-3-540-30203-2_21"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-95486-3_7"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/839268.839271"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/241388.241396"},{"key":"e_1_2_1_2_10_2","unstructured":"Habel A Pennemann KH (2005) 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. Essays dedicated to Hartmut Ehrig on the occasion of his 60th birthday. Springer Lecture Notes in Computer Science vol 3393 pp 293\u2013308"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Habel A Pennemann KH (2006) Satisfiability of high-level conditions. In: Corradini A Ehrig H Montanari U Ribeiro L Rozenberg G (eds) Graph transformations third international conference ICGT 2006. Springer Lecture Notes in Computer Science vol 4178 pp 430\u2013444","DOI":"10.1007\/11841883_30"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Habel A Pennemann KH (2008) Correctness of high-level transformation systems relative to nested conditions. Math Struct Comp Sci (accepted)","DOI":"10.1017\/S0960129508007202"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Heckel R Wagner A (1995) Ensuring consistency of conditional graph grammars\u2014a constructive approach. In: Proceedings SEGRAGRA 1995 Electr Notes Theor Comput Sci vol 2 pp 118\u2013126","DOI":"10.1016\/S1571-0661(05)80188-4"},{"key":"e_1_2_1_2_14_2","unstructured":"Jelliffe R (2000) Schematron. Internet document May 2000. http:\/\/xml.ascc.net\/resource\/schematron\/"},{"key":"#cr-split#-e_1_2_1_2_15_2.1","doi-asserted-by":"crossref","unstructured":"Lack S Sobocinski P (2004) Adhesive categories. In: Walukiewicz I","DOI":"10.1007\/978-3-540-24727-2_20"},{"key":"#cr-split#-e_1_2_1_2_15_2.2","unstructured":"(ed) Foundations of software science and computation structures 7th international conference FOSSACS 2004 Lecture Notes in Computer Science vol 2987. Springer Heidelberg pp 273-288"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Lambers L Ehrig H Orejas F (2006) Conflict detection for graph transformation with negative application conditions. In: Corradini A Ehrig H Montanari U Ribeiro L Rozenberg G (eds) Graph transformations third international conference ICGT 2006. Springer Lecture Notes in Computer Science vol 4178 pp 61\u201376","DOI":"10.1007\/11841883_6"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"De Lara J Guerra E (2008) Pattern-based model-to-model transformation. In: Ehrig H Heckel R Rozenberg G Taentzer G (eds) Graph transformations 4th international conference ICGT 2008. Springer Lecture Notes in Computer Science vol 5214 pp 426\u2013441","DOI":"10.1007\/978-3-540-87405-8_29"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Orejas F (2008) Attributed graph constraints. In: Ehrig H Heckel R Rozenberg G Taentzer G (eds) Graph transformations 4th international conference ICGT 2008. Springer Lecture Notes in Computer Science vol 5214 pp 274\u2013288","DOI":"10.1007\/978-3-540-87405-8_19"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Orejas F Ehrig H Prange U (2008) A logic of graph constraints. In: Fiadeiro JL Inverardi P (eds) Fundamental approaches to software engineering 11th international conference FASE 2008. Springer Lecture Notes in Computer Science vol 4961 pp 179\u2013198","DOI":"10.1007\/978-3-540-78743-3_14"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2004.11.002"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Pennemann KH (2008) Resolution-like theorem proving for high-level conditions. In: Ehrig H Heckel R Rozenberg G Taentzer G (eds) Graph transformations 4th international conference ICGT 2008. Lecture Notes in Computer Science vol 5214. Springer Heidelberg pp 289\u2013304","DOI":"10.1007\/978-3-540-87405-8_20"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Rensink A (2004) Representing first-order logic using graphs. In: Ehrig H Engels G Parisi-Presicce F Rozenberg G (eds) Graph transformations second international conference ICGT 2004. Springer Lecture Notes in Computer Science vol 3256 pp 319\u2013335","DOI":"10.1007\/978-3-540-30203-2_23"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/278918"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0116-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0116-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0116-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:51:19Z","timestamp":1641484279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0116-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["10.1007\/s00165-009-0116-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0116-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5]]}}}