{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:56:41Z","timestamp":1781884601961,"version":"3.54.5"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We introduce anti-pattern templates, which extend both anti-pattern matching by abstracting ground terms to variables, and unification by negative constraints. For anti-pattern templates, we study the satisfiability problem, which asks whether a given template can be instantiated to a valid anti-pattern matching instance. We show that the satisfiability problem for anti-pattern templates is NP-complete, but it becomes tractable if the number of negation symbols is bounded. Next, we consider anti-pattern templates modulo an equational theory\u00a0and discuss its relations with other variants of equational frameworks with negative constraints. In particular, we conclude that the satisfiability problem for anti-pattern templates considered modulo associativity becomes undecidable, while it is decidable modulo associativity and commutativity.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_32","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:48:01Z","timestamp":1753789681000},"page":"614-631","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Anti-pattern Templates"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8804-8011","authenticated-orcid":false,"given":"Jan","family":"Otop","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"issue":"2","key":"32_CR1","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0304-3975(94)00277-0","volume":"142","author":"F Baader","year":"1995","unstructured":"Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theor. Comput. Sci. 142(2), 229\u2013255 (1995). https:\/\/doi.org\/10.1016\/0304-3975(94)00277-0","journal-title":"Theor. Comput. Sci."},{"key":"32_CR2","doi-asserted-by":"publisher","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning (in 2 volumes), pp. 445\u2013532. MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50010-2","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"32_CR3","doi-asserted-by":"publisher","unstructured":"Balland, E., Brauner, P., Kopetz, R., Moreau, P.-E., Reilles, A.: Tom: Piggybacking Rewriting on Java. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 36\u201347. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73449-9_5","DOI":"10.1007\/978-3-540-73449-9_5"},{"issue":"1\u20132","key":"32_CR4","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236(1\u20132), 35\u2013132 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00206-6","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"32_CR5","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1016\/J.JSC.2010.01.007","volume":"45","author":"H Cirstea","year":"2010","unstructured":"Cirstea, H., Kirchner, C., Kopetz, R., Moreau, P.: Anti-patterns for rule-based languages. J. Symb. Comput. 45(5), 523\u2013550 (2010). https:\/\/doi.org\/10.1016\/J.JSC.2010.01.007","journal-title":"J. Symb. Comput."},{"key":"32_CR6","unstructured":"Comon, H.: Unification et disunification : th\u00e9orie et applications. (Unification and disunification in free algebras and in initial algebras : theory and applications). Ph.D. thesis, Grenoble Institute of Technology, France (1988), https:\/\/tel.archives-ouvertes.fr\/tel-00331263"},{"key":"32_CR7","unstructured":"Comon, H.: Disunification: A survey. In: Computational Logic - Essays in Honor of Alan Robinson. pp. 322\u2013359 (1991)"},{"key":"32_CR8","doi-asserted-by":"publisher","unstructured":"CADE 1984. LNCS, vol. 170. Springer, New York (1984). https:\/\/doi.org\/10.1007\/978-0-387-34768-4_30","DOI":"10.1007\/978-0-387-34768-4_30"},{"issue":"1","key":"32_CR9","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1006\/JSCO.1996.0041","volume":"22","author":"M Fern\u00e1ndez","year":"1996","unstructured":"Fern\u00e1ndez, M.: AC complement problems: Satisfiability and negation elimination. J. Symb. Comput. 22(1), 49\u201382 (1996). https:\/\/doi.org\/10.1006\/JSCO.1996.0041","journal-title":"J. Symb. Comput."},{"key":"32_CR10","doi-asserted-by":"publisher","unstructured":"Jez, A.: Recompression: a simple and powerful technique for word equations. In: STACS 2013. LIPIcs, vol.\u00a020, pp. 233\u2013244. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013). https:\/\/doi.org\/10.4230\/LIPICS.STACS.2013.233","DOI":"10.4230\/LIPICS.STACS.2013.233"},{"key":"32_CR11","doi-asserted-by":"publisher","unstructured":"Kirchner, C., Kopetz, R., Moreau, P.: Anti-pattern matching modulo. In: Language and Automata Theory and Applications, Second International Conference, LATA 2008, Tarragona, Spain, March 13-19, 2008. Revised Papers. pp. 275\u2013286 (2008). https:\/\/doi.org\/10.1007\/978-3-540-88282-4_26","DOI":"10.1007\/978-3-540-88282-4_26"},{"key":"32_CR12","doi-asserted-by":"publisher","unstructured":"Kounalis, E., Lugiez, D., Pottier, L.: A solution of the complement problem in associative-commutative theories. In: MFCS 1991. pp. 287\u2013297 (1991). https:\/\/doi.org\/10.1007\/3-540-54345-7_72","DOI":"10.1007\/3-540-54345-7_72"},{"issue":"4","key":"32_CR13","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0020-0190(94)00188-5","volume":"53","author":"G Kucherov","year":"1995","unstructured":"Kucherov, G., Rusinowitch, M.: Undecidability of ground reducibility for word rewriting systems with variables. Inf. Process. Lett. 53(4), 209\u2013215 (1995). https:\/\/doi.org\/10.1016\/0020-0190(94)00188-5","journal-title":"Inf. Process. Lett."},{"key":"32_CR14","doi-asserted-by":"publisher","unstructured":"Lassez, J., Maher, M.J., Marriott, K.: Elimination of negation in term algebras. In: Mathematical Foundations of Computer Science 1991, 16th International Symposium, MFCS\u201991, Kazimierz Dolny, Poland, September 9-13, 1991, Proceedings. pp. 1\u201316 (1991). https:\/\/doi.org\/10.1007\/3-540-54345-7_44","DOI":"10.1007\/3-540-54345-7_44"},{"key":"32_CR15","doi-asserted-by":"publisher","unstructured":"Lugiez, D., Moysset, J.L.: Complement problems and tree automata in ac-like theories. In: STACS 1993. pp. 515\u2013524 (1993). https:\/\/doi.org\/10.1007\/3-540-56503-5_51","DOI":"10.1007\/3-540-56503-5_51"},{"key":"32_CR16","unstructured":"Otop, J.: Unification of anti-terms. In: UNIF 2011. pp. 9\u201314 (2011)"},{"key":"32_CR17","doi-asserted-by":"publisher","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. ACM 51(3), 483\u2013496 (2004). https:\/\/doi.org\/10.1145\/990308.990312","DOI":"10.1145\/990308.990312"},{"key":"32_CR18","doi-asserted-by":"publisher","unstructured":"Ramakrishnan, I.V., Sekar, R., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning (in 2 volumes), pp. 1853\u20131964. MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50028-X","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"32_CR19","doi-asserted-by":"publisher","unstructured":"Toyama, Y.: Confluent term rewriting systems with membership conditions. In: Conditional Term Rewriting Systems. pp. 228\u2013241 (1987). https:\/\/doi.org\/10.1007\/3-540-19242-5_17","DOI":"10.1007\/3-540-19242-5_17"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:28:18Z","timestamp":1781882898000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author has no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}