{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:34:56Z","timestamp":1761597296612,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,7,20]],"date-time":"2011-07-20T00:00:00Z","timestamp":1311120000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2011,7,20]]},"DOI":"10.1145\/2003476.2003481","type":"proceedings-article","created":{"date-parts":[[2011,7,20]],"date-time":"2011-07-20T12:34:54Z","timestamp":1311165294000},"page":"5-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Incremental checking of well-founded recursive specifications modulo axioms"],"prefix":"10.1145","author":[{"given":"Felix","family":"Schernhammer","sequence":"first","affiliation":[{"name":"University of Technology, Vienna, Austria"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana-Champaign, IL, USA"}]}],"member":"320","published-online":{"date-parts":[[2011,7,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1927806.1927812"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90003-0"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/280474"},{"key":"e_1_3_2_1_4_1","volume-title":"Term Rewriting Systems","author":"Bezem M.","year":"2003","unstructured":"M. Bezem , J. Klop , and R. Vrijer , editors . Term Rewriting Systems . Cambridge Tracts in Theoretical Computer Science 55. Cambridge University Press , 2003 . M. Bezem, J. Klop, and R. Vrijer, editors. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science 55. Cambridge University Press, 2003."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00358-9"},{"key":"e_1_3_2_1_6_1","first-page":"4350","article-title":"All About Maude -- A High-Performance Logical Framework","author":"Clavel M.","year":"2007","unstructured":"M. Clavel , F. Dur\u00e1n , S. Eker , J. Meseguer , P. Lincoln , N. Mart\u00ed-Oliet and C. Talcott . All About Maude -- A High-Performance Logical Framework . LNCS 4350 , 2007 . M. Clavel, F. Dur\u00e1n, S. Eker, J. Meseguer, P. Lincoln, N. Mart\u00ed-Oliet and C. Talcott. All About Maude -- A High-Performance Logical Framework. LNCS 4350, 2007.","journal-title":"LNCS"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/648340.756212"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1807707.1807724"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1927806.1927815"},{"key":"e_1_3_2_1_11_1","series-title":"AMAST Series","volume-title":"Cafe OBJ Report. World Scientific","author":"Futatsugi K.","year":"1998","unstructured":"K. Futatsugi and R. Diaconescu . Cafe OBJ Report. World Scientific , AMAST Series , 1998 . K. Futatsugi and R. Diaconescu. Cafe OBJ Report. World Scientific, AMAST Series, 1998."},{"key":"e_1_3_2_1_12_1","first-page":"93","volume-title":"Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA'01), LNCS 2051","author":"Giesl J.","year":"2001","unstructured":"J. Giesl and D. Kapur . Dependency pairs for equational rewriting. In A. Middeldorp editor , Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA'01), LNCS 2051 , pages 93 -- 108 . Springer , 2001 . J. Giesl and D. Kapur. Dependency pairs for equational rewriting. In A. Middeldorp editor, Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA'01), LNCS 2051, pages 93--108. Springer, 2001."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_24"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_14"},{"key":"e_1_3_2_1_16_1","volume-title":"Sufficient completeness checking with propositional tree automata. Technical report","author":"Hendrix J.","year":"2005","unstructured":"J. Hendrix , H. Ohsaki , and J. Meseguer . Sufficient completeness checking with propositional tree automata. Technical report , CS Department University of Illinois at Urbana-Champaign, 2005 . http:\/\/www.ideals.illinois.edu\/handle\/2142\/11096 J. Hendrix, H. Ohsaki, and J. Meseguer. Sufficient completeness checking with propositional tree automata. Technical report, CS Department University of Illinois at Urbana-Champaign, 2005. http:\/\/www.ideals.illinois.edu\/handle\/2142\/11096"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1137\/0215084"},{"issue":"1","key":"e_1_3_2_1_19_1","first-page":"61","article-title":"Modular Church-Rosser modulo: the complete picture","volume":"2","author":"Jouannaud J.-P.","year":"2008","unstructured":"J.-P. Jouannaud and Y. Toyama . Modular Church-Rosser modulo: the complete picture . International Journal of Software and Informatics , 2 ( 1 ): 61 -- 75 , 2008 . J.-P. Jouannaud and Y. Toyama. Modular Church-Rosser modulo: the complete picture. International Journal of Software and Informatics, 2(1):61--75, 2008.","journal-title":"International Journal of Software and Informatics"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-46508-1_3","volume-title":"Selected Papers from Automated Deduction in Classical and Non-Classical Logics LNCS 1761","author":"Kapur D.","year":"2000","unstructured":"D. Kapur and G. Sivakumar . Proving associative-communicative termination using RPO-compatible orderings . In Selected Papers from Automated Deduction in Classical and Non-Classical Logics LNCS 1761 pages 39 -- 61 , Springer 2000 . D. Kapur and G. Sivakumar. Proving associative-communicative termination using RPO-compatible orderings. In Selected Papers from Automated Deduction in Classical and Non-Classical Logics LNCS 1761 pages 39--61, Springer 2000."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-19488-6_123","volume-title":"Proceedings of the 15th International Colloquium on Automata, Languages and Programming (ICALP'88)","author":"Kirchner C.","year":"1988","unstructured":"C. Kirchner , H. Kirchner , and J. Meseguer . Operational semantics of OBJ3. In T. Lepist\u00f6 and A. Salomaa editors , Proceedings of the 15th International Colloquium on Automata, Languages and Programming (ICALP'88) , LNCS 317, pages 287 -- 301 . Springer , 1988 . C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ3. In T. Lepist\u00f6 and A. Salomaa editors, Proceedings of the 15th International Colloquium on Automata, Languages and Programming (ICALP'88), LNCS 317, pages 287--301. Springer, 1988."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316050"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2004.02.003"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/513717"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647708.734928"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/322248.322251"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00075-8"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_18"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03177743"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/547871"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00366-8"}],"event":{"name":"PPDP '11: Symposium on Principles and Practices of Declarative Programming","sponsor":["University of Southern Denmark","Danish Agency for Science Technology and Innovation DASTI","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Odense Denmark","acronym":"PPDP '11"},"container-title":["Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2003476.2003481","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2003476.2003481","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:06:22Z","timestamp":1750244782000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2003476.2003481"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,20]]},"references-count":31,"alternative-id":["10.1145\/2003476.2003481","10.1145\/2003476"],"URL":"https:\/\/doi.org\/10.1145\/2003476.2003481","relation":{},"subject":[],"published":{"date-parts":[[2011,7,20]]},"assertion":[{"value":"2011-07-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}