{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:57:44Z","timestamp":1725551864706},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540317821"},{"type":"electronic","value":"9783540317845"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11663881_2","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T11:31:46Z","timestamp":1137670306000},"page":"2-21","source":"Crossref","is-referenced-by-count":0,"title":["Equational Constraint Solving Via a Restricted Form of Universal Quantification"],"prefix":"10.1007","author":[{"given":"Javier","family":"\u00c1lvez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paqui","family":"Lucio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"\u00c1lvez, J., Lucio, P.: Equational constraint solving using quasi-solved forms. In: Proceedings of the 18th International Workshop on Unification (UNIF 2004), Cork, Ireland, June 5 (2004)"},{"key":"2_CR2","unstructured":"Baumgartner, P., Stenz, G.: Instance based methods. In: Tutorial T3.- 2nd Int. Joint Conf. on Automated Reasoning, IJCAR 2004, Cork, Ireland (2004)"},{"key":"2_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"issue":"4","key":"2_CR4","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1145\/179812.179813","volume":"41","author":"W.L. Buntine","year":"1994","unstructured":"Buntine, W.L., B\u00fcrckert, H.-J.: On solving equations and disequations. Journal of the ACM\u00a041(4), 591\u2013629 (1994)","journal-title":"Journal of the ACM"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0018439","volume-title":"Logics in AI","author":"R. Caferra","year":"1991","unstructured":"Caferra, R., Zabel, N.: Extending resolution for model construction. In: van Eijck, J. (ed.) JELIA 1990. LNCS, vol.\u00a0478, pp. 153\u2013169. Springer, Heidelberg (1991)"},{"issue":"6","key":"2_CR6","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"Caferra, R., Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. J. Symb. Comput.\u00a013(6), 613\u2013641 (1992)","journal-title":"J. Symb. Comput."},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-45349-0_14","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"A. Colmerauer","year":"2000","unstructured":"Colmerauer, A., Dao, T.-B.-H.: Expresiveness of full first order constraints in the algebra of finite and infinite trees. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 172\u2013186. Springer, Heidelberg (2000)"},{"key":"2_CR8","unstructured":"Comon, H.: Disunification: A survey. In: Lassez, J.L., Plotkin, G. (eds.) Essays in Honour of Alan Robinson (1991)"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation\u00a07, 371\u2013425 (1989)","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(90)90080-L","volume":"48","author":"K.J. Compton","year":"1990","unstructured":"Compton, K.J., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. Ann. Pure Appl. Logic\u00a048(1), 1\u201379 (1990)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"2_CR11","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C.G. Ferm\u00fcller","year":"1996","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Hyperresolution and automated model building. J. Log. Comput.\u00a06(2), 173\u2013203 (1996)","journal-title":"J. Log. Comput."},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2003.1210045","volume-title":"Proc. 18th IEEE Symposium on Logic in Computer Science","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposium on Logic in Computer Science, pp. 55\u201364. IEEE Computer Society Press, Los Alamitos (2003)"},{"issue":"3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/BF00243794","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reasoning\u00a03(3), 301\u2013317 (1987)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proc. of the 3rd IEEE Symp. on Logic in Computer Science, pp. 348\u2013357. Computer Society Press (1988)","DOI":"10.1109\/LICS.1988.5132"},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1016\/S0049-237X(08)70560-3","volume-title":"The Metamathematics of Algebraic Systems (Collected Papers: 1936-1967), ch. 23","author":"A.I. Malcev","year":"1971","unstructured":"Malcev, A.I.: Axiomatizable classes of locally free algebras. In: Wells, B.F. (ed.) The Metamathematics of Algebraic Systems (Collected Papers: 1936-1967), ch. 23, vol.\u00a066, pp. 262\u2013281. North-Holland, Amsterdam (1971)"},{"key":"2_CR16","unstructured":"Peltier, N.: Nouvelles Techniques pour la Construction de Mod\u00e8les finis ou infinis en D\u00e9duction Automatique. PhD thesis, Institut National Polytechnique de Grenoble (1997)"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/BFb0054252","volume-title":"CADE-15: Proceedings of the 15th International Conference on Automated Deduction","author":"N. Peltier","year":"1998","unstructured":"Peltier, N.: System description: An equational constraints solver. In: CADE-15: Proceedings of the 15th International Conference on Automated Deduction, London, UK, pp. 119\u2013123. Springer, Heidelberg (1998)"},{"key":"2_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-48660-7_7","volume-title":"Automated Deduction - CADE-16","author":"R. Pichler","year":"1999","unstructured":"Pichler, R.: Solving equational problems efficiently. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 97\u2013111. Springer, Heidelberg (1999)"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/S0747-7171(03)00029-4","volume":"36","author":"R. Pichler","year":"2003","unstructured":"Pichler, R.: On the complexity of equational problems in CNF. Journal of Symbolic Computation\u00a036, 235\u2013269 (2003)","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"2_CR20","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1145\/371316.371494","volume":"2","author":"T. Rybina","year":"2001","unstructured":"Rybina, T., Voronkov, E.: A decision procedure for term algebras with queues. ACM Trans. Comput. Logic\u00a02(2), 155\u2013181 (2001)","journal-title":"ACM Trans. Comput. Logic"},{"key":"2_CR21","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-61511-3_91","volume-title":"Automated Deduction - Cade-13","author":"S. Vorobyov","year":"1996","unstructured":"Vorobyov, S.: An improved lower bound for the elementary theories of trees. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 275\u2013287. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Information and Knowledge Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11663881_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:12:48Z","timestamp":1619507568000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11663881_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540317821","9783540317845"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/11663881_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}