{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,12]],"date-time":"2025-08-12T21:27:46Z","timestamp":1755034066391,"version":"3.32.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2004,7,1]],"date-time":"2004-07-01T00:00:00Z","timestamp":1088640000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2004,7]]},"DOI":"10.1007\/s10817-004-2279-7","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T13:28:22Z","timestamp":1109770102000},"page":"1-28","source":"Crossref","is-referenced-by-count":9,"title":["Unification Modulo ACUI Plus Distributivity Axioms"],"prefix":"10.1007","volume":"33","author":[{"given":"Siva","family":"Anantharaman","sequence":"first","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Rusinowitch","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Aiken, A. and Wimmers, E.: Solving systems of set constraints, in Proc. 7th IEEE Symposium on Logic in Computer Science (LICS?92), 1992, pp. 329?340.","DOI":"10.1109\/LICS.1992.185545"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Aiken, A., Kozen, D., Vardi, M. and Wimmers, E.: The complexity of set constraints, in Proc. Conf. CSL?93, EACSL, September 1993, pp. 1?18.","DOI":"10.1007\/BFb0049320"},{"key":"CR3","unstructured":"Anantharaman, S., Narendran, P. and Rusinowitch, M.: Unification over ACUI plus distributivity\/homomorphisms, in Proc. CADE-19, LNAI 2741, Springer-Verlag, pp. 442?458."},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Anantharaman, S., Narendran, P. and Rusinowitch, M.: ACID-unification is NEXPTIME-decidable, in Proc. MFCS?03, LNCS 2747, Springer-Verlag, pp. 169?179.","DOI":"10.1007\/978-3-540-45138-9_11"},{"key":"CR5","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1016\/S0747-7171(89)80055-0","volume":"8","author":"F. Baader","year":"1989","unstructured":"Baader, F.: Unification in commutative theories, J. Symbolic Comput. 8 (1989), 479?497.","journal-title":"J. Symbolic Comput."},{"issue":"3","key":"CR6","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1006\/jsco.2000.0426","volume":"31","author":"F. Baader","year":"2001","unstructured":"Baader, F. and Narendran, P.: Unification of concept terms in description logics, J. Symbolic Comput. 31(3) (2001), 277?305.","journal-title":"J. Symbolic Comput."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Baader, F. and Schulz, K. U.: Unification in the union of disjoint equational theories: Combining decision procedures, in Proc. 11th Conference on Automated Deduction (CADE-11), Saratoga Springs (NY), LNAI 607, Springer-Verlag, 1992, pp. 50?65.","DOI":"10.1007\/3-540-55602-8_155"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H. and Waldmann, U.: Set constraints are the monadic class, in Proc. 8th IEEE Symposium on Logic in Computer Science (LICS?93), 1993, pp. 75?83.","DOI":"10.1109\/LICS.1993.287598"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Charatonik, W. and Podelski, A.: Set constraints with intersection, in Proc. 12th IEEE Symposium on Logic in Computer Science (LICS?97), Warsaw, 1997, pp. 362?372. (To appear in Information and Computation.)","DOI":"10.1109\/LICS.1997.614962"},{"key":"CR10","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S. and Tommasi, M.: Tree automata techniques and applications, http:\/\/www.grappa.univ-lille3.fr\/tata\/"},{"key":"CR11","unstructured":"Focardi, R.: Analysis and automatic detection of information flows and network systems, Doctoral Thesis, Technical Report UBLCS-99-16, University of Bologna, July 1999."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Gilleron, R., Tison, S. and Tommasi, M.: Solving systems of set constraints using tree automata, in Proc. STACS?93, LNCS 665, Springer-Verlag, pp. 505?514.","DOI":"10.1007\/3-540-56503-5_50"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2747","volume":"149","author":"R. Gilleron","year":"1999","unstructured":"Gilleron, R., Tison, S. and Tommasi, M.: Set constraints and tree automata, Inform. and Comput. 149 (1999), 1?41 (see also Tech. Report IT 292, Laboratoire-LIFL, Lille, 1996).","journal-title":"Inform. and Comput."},{"key":"CR14","volume-title":"Computation: Finite and Infinite Machines","author":"M. Minsky","year":"1972","unstructured":"Minsky, M.: Computation: Finite and Infinite Machines, Prentice-Hall, London, 1972."},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Narendran, P.: On solving linear equations over polynomial semirings, in Proc. 11th Annual Symp. on Logic in Computer Science, July 1996, pp. 466?472.","DOI":"10.1109\/LICS.1996.561463"},{"key":"CR16","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/BF00247671","volume":"17","author":"P. Narendran","year":"1996","unstructured":"Narendran, P. and Rusinowitch, M.: Any ground associative-commutative theory has a finite canonical system, J. Automated Reasoning 17 (1996), 131?143.","journal-title":"J. Automated Reasoning"},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"Nutt, W.: Unification in monoidal theories, in M. Stickel (ed.), Proc. CADE-10, LNAI 449, Springer-Verlag, pp. 618?632.","DOI":"10.1007\/3-540-52885-7_118"},{"issue":"3","key":"CR18","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1006\/jsco.1996.0054","volume":"22","author":"M. Schmidt-Schauss","year":"1997","unstructured":"Schmidt-Schauss, M.: Decidability of unification in the theory of one-sided distributivity and a multiplicative unit, J. Symbolic Comput. 22(3) (1997), 315?344.","journal-title":"J. Symbolic Comput."},{"issue":"1?2","key":"CR19","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/S0304-3975(98)00081-4","volume":"208","author":"M. Schmidt-Schauss","year":"1998","unstructured":"Schmidt-Schauss, M.: A decision algorithm for distributive unification, Theoret. Comput. Sci. 208(1?2) (1998), 111?148.","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"CR20","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0020-0190(94)00130-8","volume":"52","author":"H. Seidl","year":"1994","unstructured":"Seidl, H.: Haskell overloading is DEXPTIME-complete, Inform. Process. Lett. 52(2) (1994), 57?60.","journal-title":"Inform. Process. Lett."},{"issue":"2","key":"CR21","doi-asserted-by":"crossref","first-page":"402","DOI":"10.2307\/2274856","volume":"54","author":"J. Siekmann","year":"1989","unstructured":"Siekmann, J. and Szabo, P.: The undecidability of DA-unification problem, J. Symbolic Logic 54(2) (1989), 402?414.","journal-title":"J. Symbolic Logic"},{"issue":"1?2","key":"CR22","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1023\/A:1009826603139","volume":"5","author":"J.-M. Talbot","year":"2000","unstructured":"Talbot, J.-M., Devienne, Ph. and Tison, S.: Generalized Definite Set Constraints, In CONSTRAINTS: An International Journal 5(1?2): 161?202, 2000.","journal-title":"CONSTRAINTS: An International Journal"},{"issue":"1?2","key":"CR23","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S0747-7171(87)80026-3","volume":"3","author":"E. Tiden","year":"1987","unstructured":"Tiden, E. and Arnborg, S.: Unification Problems with One-sided Distributivity, Journal of Symbolic Computation 3(1?2): 183?202, 1987.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-2279-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-004-2279-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-2279-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,25]],"date-time":"2024-12-25T10:54:20Z","timestamp":1735124060000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-004-2279-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,7]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["5382279"],"URL":"https:\/\/doi.org\/10.1007\/s10817-004-2279-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2004,7]]}}}