{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T14:06:44Z","timestamp":1763388404145},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[1992,3]]},"DOI":"10.1007\/bf01189020","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T10:58:48Z","timestamp":1108724328000},"page":"1-26","source":"Crossref","is-referenced-by-count":20,"title":["Narrowing based procedures for equational disunification"],"prefix":"10.1007","volume":"3","author":[{"given":"Maribel","family":"Fern\ufffdndez","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L.: Proof by consistency in equational theories. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988","DOI":"10.1109\/LICS.1988.5122"},{"key":"CR2","volume-title":"Lecture Notes in Computer Sciences, vol. 213","author":"D. Bert","year":"1986","unstructured":"Bert, D., Echahed, R.: Design and implementation of a generic, logic and functional programming language. In: Proc. ESOP 86, Saarbr\u00fccken. Lecture Notes in Computer Sciences, vol. 213. Berlin, Heidelberg, New York: Springer, March 1986. Available as IMAG Research Report 560"},{"key":"CR3","unstructured":"Bogaert, B.: Automates d'arbres avec tests d'r\u00e9galit\u00e9s. PhD thesis, Universit\u00e9 des Sciences et Techniques de Lille Flandres-Artois, December 1990"},{"key":"CR4","volume-title":"Lecture Notes in Computer Sciences, vol. 310","author":"H.J. B\u00fcrckert","year":"1988","unstructured":"B\u00fcrckert, H.J.: Solving disequations in equational theories. In: Proc. 9th Conf. on Automated Deduction, Argonne. Lecture Notes in Computer Sciences, vol. 310. Berlin, Heidelberg, New York: Springer, May 1988"},{"key":"CR5","unstructured":"Colmerauer, A.: Equations and inequations on finite and infinite trees. In: FGCS'84 Proceedings, pages 85?99, November 1984"},{"key":"CR6","unstructured":"Colmerauer, A.: Opening the Prolog III universe. Byte Magazine, 1987"},{"key":"CR7","volume-title":"Th\u00e8se de Doctorat","author":"H. Comon","year":"1988","unstructured":"Comon, H.: Unification et disunification: Th\u00e9orie et applications. Th\u00e8se de Doctorat, Institut National Polytechnique de Grenoble, France, 1988"},{"key":"CR8","first-page":"76","volume-title":"Lecture Notes in Computer Sciences, vol 355","author":"H. Comon","year":"1989","unstructured":"Comon, H.: Inductive proofs by specifications transformation. In Proc. 3rd Rewriting Techniques and Applications 89, Chapel Hill. Lecture Notes in Computer Sciences, vol 355, pp. 76?91. Berlin, Heidelberg, New York: Springer, April 1989"},{"key":"CR9","volume-title":"Proc. ICALP, Madrid. Lecture Notes in Computer Sciences, vol. 510","author":"H. Comon","year":"1991","unstructured":"Comon, H.: Complete axiomatizations of some quotient term algebras. In: Proc. ICALP, Madrid. Lecture Notes in Computer Sciences, vol. 510. Berlin, Heidelberg, New York: Springer, July 1991"},{"key":"CR10","unstructured":"Comon, H.: Disunification: a survey. In: Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991"},{"key":"CR11","unstructured":"Dershowitz, N.: Applications of the Knuth-Bendix completion procedure. In Proceedings of the Seminaire d'Informatique Theorique, pp. 95?111, Paris, France, December 1982"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243?309. North-Holland 1990","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"CR13","volume-title":"Lecture Notes in Computer Sciences, vol. 159","author":"F. Fages","year":"1983","unstructured":"Fages, F., Huet, G.: Unification and matching in equational theories. In Proc. 8th. Coll. on Trees and Algebra in Programming. Lecture Notes in Computer Sciences, vol. 159, l'Aquila, Italy, 1983. Berlin, Heidelberg, New York: Springer"},{"key":"CR14","unstructured":"Fay, M.: First-order unification in an equational theory. In: Proceedings 4th Workshop on Automated Deduction, Austin, Texas, pp. 161?167, 1979"},{"key":"CR15","unstructured":"Fern\u00e1ndez, M., Levy, F.: Disunification in equational theories. In Proceedings 10th International Conference of the Chilean Computer Science Society, Chile, 1990"},{"key":"CR16","first-page":"105","volume-title":"Lecture Notes in Computer Sciences, vol. 226","author":"L. Fribourg","year":"1986","unstructured":"Fribourg, L.: A strong restriction of the inductive completion procedure. In Proc. 13th ICALP, Rennes. Lecture Notes in Computer Sciences, vol. 226, pp. 105?115. Berlin, Heidelberg, New York: Springer 1986"},{"key":"CR17","first-page":"295","volume-title":"Logic Programming: Functions, Relations, and Equations","author":"J. Goguen","year":"1986","unstructured":"Goguen, J., Meseguer, J.: EQLOG: Equality, types, and generic modules for logic programming, In: DeGroot, D., Lindstrom, G. (ed.) Logic Programming: Functions, Relations, and Equations, pp. 295?363. Prentice Hall, Berlin, Heidelberg, New York: Springer 1986"},{"key":"CR18","series-title":"Report R-82-1113","volume-title":"PhD thesis","author":"J. Hsiang","year":"1982","unstructured":"Hsiang, J.: Topics in Automated Theorem Proving and Program Generation. PhD thesis, Department of Computer Science, University of Illinois, Urbana, IL, December 1982. Report R-82-1113"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Huet, G., Hullot, J.-M.: Proofs by induction in equational theories with constructors. J. Comput. Syst. Sci., 25(2), 1982","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/B978-0-12-115350-2.50017-8","volume-title":"Formal Language Theory: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"Huet, G., Oppen, D.: Equations and rewrite rules: a survey. In: Book, R. (ed.), Formal Language Theory: Perspectives and Open Problems, pp. 349?405. New York: Academic Press 1980"},{"key":"CR21","volume-title":"Lecture Notes in Computer Sciences, vol. 87","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In Proc. 5th Conf. on Automated Deduction, Les Arcs, Lecture Notes in Computer Sciences, vol. 87. Berlin, Heidelberg, New York: Springer, July 1980"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: Proc. 14th ACM Symp. Principles of Programming Languages, Munich, 1987","DOI":"10.1145\/41625.41635"},{"key":"CR23","unstructured":"Jouannaud, J.-P., Kirchner, C: Solving equations in abstract algebras: A rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds). Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, 1991 (to appear)"},{"key":"CR24","first-page":"361","volume-title":"Lecture Notes in Computer Sciences, vol. 154","author":"J.-P. Jouannaud","year":"1983","unstructured":"Jouannaud, J.-P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In Proc. 10th Int. Conf. on Automata, Languages and Programming, Barcelona, Lecture Notes in Computer Sciences, vol. 154, pp. 361?373. Berlin, Heidelberg, New York: Springer 1983"},{"key":"CR25","volume-title":"Lecture Notes in Computer Sciences, vol. 343","author":"J.-P. Jouannaud","year":"1988","unstructured":"Jouannaud, J.-P., Kirchner, H., Kirchner, C., Megrelis, A.: OBJ: Programming with equalities, subsorts, ?overloading and parametrization?. In: Proc. 1st Workshop on Algebraic and Logic Programming, Gaussig, Lecture Notes in Computer Sciences, vol. 343. Berlin, Heidelberg, New York: Springer, November 1988. To appear in Journal of Logic Programming."},{"key":"CR26","unstructured":"Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in equational theories without constructors. In: Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., June 1986"},{"key":"CR27","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF01893885","volume":"28","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Rosenkratz, D., Zang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica28, 311?350 (1991)","journal-title":"Acta Informatica"},{"issue":"4","key":"CR28","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P., Zhang, H.: On sufficient completeness and related properties of term rewriting systems Acta Informatica 24(4), 395?415 (1987)","journal-title":"Acta Informatica"},{"key":"CR29","first-page":"348","volume-title":"Lecture Notes in Computer Sciences, vol. 204","author":"E. Kounalis","year":"1985","unstructured":"Kounalis, E.: Completeness in data type specifications. In: Proc. EUROCAL 85, Linz, Lecture Notes in Computer Sciences, vol. 204, pp. 348?362. Berlin, Heidelberg, New York: Springer, April 1985"},{"key":"CR30","volume-title":"Lecture Notes in Computer Sciences, vol. 488.","author":"S. Krischer","year":"1991","unstructured":"Krischer, S., Bockmayr, A.: Detecting redundant narrowing derivations by the LSE-SL reducibility test. In: Proc. 4th Rewriting Techniques and Applications 91, Como, Lecture Notes in Computer Sciences, vol. 488. Berlin, Heidelberg, New York: Springer, April 1991"},{"key":"CR31","volume-title":"Lecture Notes in Computer Sciences, vol. 306","author":"J.-L. Lassez","year":"1986","unstructured":"Lassez, J.-L., Maher, M.J., Marriot, K.G.: Unification revisited. In: Proc. Workshop on Found. of Logic and Functional Programming, Trento, Lecture Notes in Computer Sciences, vol. 306. Berlin, Heidelberg, New York: Springer, December 1986"},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, pp. 348?357, July 1988","DOI":"10.1109\/LICS.1988.5132"},{"key":"CR33","doi-asserted-by":"crossref","unstructured":"Minsky, M.L.: Recursive unsolvability of Post's problem of tag and other topics in theory of Turing machines. Annals Math. 74 (1961)","DOI":"10.2307\/1970290"},{"key":"CR34","doi-asserted-by":"crossref","unstructured":"Musser, D.: Proving inductive properties of abstract data types. In: Proc. 7th ACM Symp. Principles of Programming Languages, Las Vegas, 1980","DOI":"10.1145\/567446.567461"},{"key":"CR35","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"Plaisted, D.: Semantic confluence tests and completion methods. Information and Control65, 182?215 (1985)","journal-title":"Information and Control"},{"key":"CR36","volume-title":"Lecture Notes in Computer Sciences, vol. 202","author":"P. Rety","year":"1985","unstructured":"Rety, P., Kirchner, C., Kirchner, H., Lescanne, P.: Narrower: A new algorithm for unification and its application to logic programming. In: Proc. Rewriting Techniques and Applications 85, Dijon, Lecture Notes in Computer Sciences, vol. 202. Berlin, Heidelberg, New York: Springer, 1985."},{"key":"CR37","volume-title":"Lecture Notes in Computer Sciences, vol. 256","author":"P. Rety","year":"1987","unstructured":"Rety, P.: Improving basic narrowing techniques and commutation properties. In Proc. Rewriting Techniques and Applications 87, Bordeaux, Lecture Notes in Computer Sciences, vol. 256. Berlin, Heidelberg, New York: Springer, May 1987"},{"key":"CR38","first-page":"297","volume-title":"Resolution of Equations in Algebraic Structures, Vol. 2, Rewriting Techniques","author":"G. Smolka","year":"1989","unstructured":"Smolka, G., Nutt, W., Goguen, J.A., Meseguer, J.: Order-Sorted Equational Computation. In: Hassan A\u00eft-Kaci, Maurice Nivat, (eds), Resolution of Equations in Algebraic Structures, Vol. 2, Rewriting Techniques, Chap. 10, pp. 297?367. New York: Academic Press 1989"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01189020.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01189020\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01189020","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T16:41:49Z","timestamp":1556728909000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01189020"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["BF01189020"],"URL":"https:\/\/doi.org\/10.1007\/bf01189020","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}