{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:52:37Z","timestamp":1725663157150},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167808"},{"type":"electronic","value":"9783540398615"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16780-3_96","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:58:53Z","timestamp":1330178333000},"page":"272-280","source":"Crossref","is-referenced-by-count":1,"title":["Using narrowing to do isolation in symbolic equation solving \u2014 an experiment in automated reasoning"],"prefix":"10.1007","author":[{"given":"A. J. J.","family":"Dick","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R. J.","family":"Cunningham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF00264228","volume":"22","author":"R. J. Cunningham","year":"1983","unstructured":"R. J. Cunningham and A. J. J. Dick, \u201cRewrite Systems on a Lattice of Types,\u201d Acta Informatica 22, pp. 149\u2013169 (1983).","journal-title":"Acta Informatica"},{"key":"22_CR2","unstructured":"A. J. J. Dick, \u201cERIL \u2014 Equational Reasoning: an Interactive Laboratory,\u201d Report No. RAL86010, Rutherford Appleton Laboratory, Chilton, OX11 0QX (1986)."},{"key":"22_CR3","volume-title":"Equational Reasoning and Rewrite Systems on a Lattice of Types","author":"A. J. J. Dick","year":"1986","unstructured":"A. J. J. Dick, \u201cEquational Reasoning and Rewrite Systems on a Lattice of Types,\u201d PhD. Thesis, Dept. Computing, Imperial College, London (1986)."},{"key":"22_CR4","unstructured":"R. Forgaard and J.V. Guttag, \u201cREVE: A term Rewriting System Generator with Failure Resistant Knuth-Bendix,\u201d pp. 33\u201356 in Proceedings of an NSF workshop on the rewrite rule laboratory (Apr. 1984)."},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"G. Huet and D. C. Oppen, \u201cEquations and Rewrite Rules \u2014 A Survey,\u201d STAN-CS-80-785 (1980).","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"22_CR6","volume-title":"Recursive Decomposition Ordering","author":"J-P. Jouannoud","year":"1982","unstructured":"J-P. Jouannoud, P. Lescanne, and F. Reinig, \u201cRecursive Decomposition Ordering,\u201d Conf. on Formal Description of Programming Concepts, North Holland (1982)."},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P. B. Bendix, \u201cSimple Word Problems in Universal Algrebras,\u201d pp. 263\u2013297 in Computational Problems in Abstract Algebra, ed. J. Leech, Pergamon Press (1970).","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"P. Lescanne, \u201cComputer Experiments with the REVE Term Rewriting System Generator,\u201d pp. 99\u2013108 in Proc. 10th Symp. on Principles of Programming Languages, ACM Austin, TX (1983 ).","DOI":"10.1145\/567067.567078"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"P. Rety, C. Kirchner, H. Kirchner, and P. Lescanne, \u201cNARROWER: a new algorithm for unification and its application to Logic Programming,\u201d To appear in Procs. of the First Internat. Conf. on Rewriting Techniques and Applications, LNCS, Springer-Verlag (May 1985).","DOI":"10.1007\/3-540-15976-2_7"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"L. Sterling, A. Bundy, L. Byrd, R. O'Keefe, and B. Silver, \u201cSolving Symbolic Equations with PRESS,\u201d Univ. of Edinburgh, Dept. of Artificial Intelligence, Research Paper No: 171 (Jan. 1982).","DOI":"10.1007\/3-540-11607-9_13"}],"container-title":["Lecture Notes in Computer Science","8th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16780-3_96.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T13:44:49Z","timestamp":1687268689000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16780-3_96"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167808","9783540398615"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-16780-3_96","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}