{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:49:54Z","timestamp":1725475794150},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_38","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"465-481","source":"Crossref","is-referenced-by-count":1,"title":["On Unification for Bounded Distributive Lattices"],"prefix":"10.1007","author":[{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"38_CR1","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/S0020-0190(98)00106-9","volume":"67","author":"F. Baader","year":"1998","unstructured":"Baader, F.: On the complexity of Boolean unification. Information Processing Letters\u00a067(4), 215\u2013220 (1998)","journal-title":"Information Processing Letters"},{"key":"38_CR2","first-page":"331","volume-title":"Proceedings of ECAI 1998","author":"F. Baader","year":"1998","unstructured":"Baader, F., Narendran, P.: Unification of concept terms in description logics. In: Prade, H. (ed.) Proceedings of ECAI 1998, pp. 331\u2013335. Wiley, Chichester (1998)"},{"key":"38_CR3","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. J. Symbolic Computation\u00a021, 211\u2013243 (1996)","journal-title":"J. Symbolic Computation"},{"key":"38_CR4","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0304-3975(97)00147-3","volume":"192","author":"F. Baader","year":"1998","unstructured":"Baader, F., Schulz, K.U.: Combination of constraint solvers for free and quasifree structures. Theoretical Computer Science\u00a0192, 107\u2013161 (1998)","journal-title":"Theoretical Computer Science"},{"key":"38_CR5","volume-title":"Handbook of Automated Reasoning","author":"F. Baader","year":"2000","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier, Amsterdam (2000) (to appear)"},{"key":"38_CR6","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1109\/LICS.1993.287598","volume-title":"Eighth Annual IEEE Symposium on Logic in Computer Science","author":"L. Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Set constraints are the monadic class. In: Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, June 19-23, pp. 75\u201383. IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/3-540-55124-7_6","volume-title":"Word Equations and Related Topics","author":"A. Bockmayr","year":"1992","unstructured":"Bockmayr, A.: Algebraic and logical aspects of unification. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol.\u00a0572, pp. 171\u2013180. Springer, Heidelberg (1992)"},{"key":"38_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/3-540-55124-7_7","volume-title":"Word Equations and Related Topics","author":"A. Bockmayr","year":"1992","unstructured":"Bockmayr, A.: Model-theoretic aspects of unification. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol.\u00a0572, pp. 181\u2013196. Springer, Heidelberg (1992)"},{"key":"38_CR9","series-title":"LNAI","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-55034-8","volume-title":"A resolution principle for a logic with restricted quantifiers","author":"H.J. B\u00fcrckert","year":"1991","unstructured":"B\u00fcrckert, H.J.: A Resolution Principle for a Logic with Restricted Quantifiers. LNCS (LNAI), vol.\u00a0568. Springer, Heidelberg (1991)"},{"key":"38_CR10","volume-title":"Graduate Texts in Mathematics","author":"S. Burris","year":"1981","unstructured":"Burris, S., Sankappanavar, H.P.: A Course in Universal Algebra. In: Graduate Texts in Mathematics. Springer, Heidelberg (1981)"},{"issue":"3","key":"38_CR11","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W.F. Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Programming\u00a01(3), 267\u2013284 (1984)","journal-title":"J. Logic Programming"},{"issue":"2","key":"38_CR12","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0304-3975(94)90011-6","volume":"126","author":"J.A. Gerhard","year":"1994","unstructured":"Gerhard, J.A., Petrich, M.: Unification in free distributive lattices. Theoretical Computer Science\u00a0126(2), 237\u2013257 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"38_CR13","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1093\/logcom\/7.6.733","volume":"7","author":"S. Ghilardi","year":"1997","unstructured":"Ghilardi, S.: Unification through projectivity. J. Logic and Computation\u00a07(6), 733\u2013752 (1997)","journal-title":"J. Logic and Computation"},{"issue":"1","key":"38_CR14","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1137\/0216011","volume":"16","author":"H.B. Hunt","year":"1987","unstructured":"Hunt, H.B., Rosenkrantz, D.J., Bloniarz, P.A.: On the computational complexity of algebra of lattices. SIAM Journal of Computation\u00a016(1), 129\u2013148 (1987)","journal-title":"SIAM Journal of Computation"},{"issue":"1","key":"38_CR15","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1137\/0219003","volume":"19","author":"H.B. Hunt","year":"1990","unstructured":"Hunt, H.B., Stearns, R.E.: The complexity of very simple Boolean formulas with applications. SIAM J. Comput.\u00a019(1), 44\u201370 (1990)","journal-title":"SIAM J. Comput."},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"Kirchner, C., Kirchner, H.: Constrained equational reasoning. In: UNIF 1989 Extended Abstacts of the 3rd Int. Workshop on Unification, Pfalzakademie, Lambrecht, pp. 160\u2013171 (1989)","DOI":"10.1145\/74540.74585"},{"key":"38_CR17","series-title":"LNAI","first-page":"477","volume-title":"Automated Deduction - CADE-11","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering constrained clauses. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 477\u2013491. Springer, Heidelberg (1992)"},{"key":"38_CR18","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1112\/plms\/s3-24.3.507","volume":"3","author":"H.A. Priestley","year":"1972","unstructured":"Priestley, H.A.: Ordered topological spaces and the representation of distributive lattices. Proc. London Math. Soc.\u00a03, 507\u2013530 (1972)","journal-title":"Proc. London Math. Soc."},{"issue":"1\u20132","key":"38_CR19","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0304-3975(98)00081-4","volume":"208","author":"M. Schmidt-Schau\u00df","year":"1998","unstructured":"Schmidt-Schau\u00df, M.: A decision algorithm for distributive unification. Theoretical Computer Science\u00a0208(1\u20132), 111\u2013148 (1998)","journal-title":"Theoretical Computer Science"},{"key":"38_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/3-540-48660-7_11","volume-title":"Automated Deduction - CADE-16","author":"V. Sofronie-Stokkermans","year":"1999","unstructured":"Sofronie-Stokkermans, V.: On the universal theory of varieties of distributive lattices with operators: Some decidability and complexity results. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 157\u2013171. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T10:26:26Z","timestamp":1553336786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/10721959_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}