{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:52:44Z","timestamp":1725663164131},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540186250"},{"type":"electronic","value":"9783540480334"}],"license":[{"start":{"date-parts":[[1987,1,1]],"date-time":"1987-01-01T00:00:00Z","timestamp":536457600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1987]]},"DOI":"10.1007\/3-540-18625-5_57","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:40:27Z","timestamp":1330198827000},"page":"305-325","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning in systems of equations and inequations"],"prefix":"10.1007","author":[{"given":"Chilukuri K.","family":"Mohan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mandayam K.","family":"Srivas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"J.A.Bergstra, J.W.Klop, Conditional Rewrite Rules: Confluence and Termination, Journal of Computer & System Sciences 32, No.3, June 1986.","DOI":"10.1016\/0022-0000(86)90033-4"},{"key":"21_CR2","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1017\/S0305004100013463","volume":"31","author":"G. Birkhoff","year":"1935","unstructured":"G. Birkhoff, On the Structure of Abstract Algebras, Proc. Cambridge Philos. Soc. 31, 433\u2013454, 1935.","journal-title":"Proc. Cambridge Philos. Soc."},{"key":"21_CR3","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"C.L. Chang, R.C. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"21_CR4","volume-title":"Proc. Intl. Conf. on Fifth Generation Computer Systems","author":"A. Colmerauer","year":"1984","unstructured":"A. Colmerauer, Equations and Inequations on Finite and Infinite Trees, Proc. Intl. Conf. on Fifth Generation Computer Systems, ICOT, Japan, 1984."},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"H.Comon, Sufficient Completeness, Term Rewriting Systems, and \u2018Anti-Unification', Eighth Conference on Automated Deduction, Oxford, LNCS 230, Springer Verlag, July 1986.","DOI":"10.1007\/3-540-16780-3_85"},{"issue":"1","key":"21_CR6","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/357153.357158","volume":"4","author":"C. M. Hoffman","year":"1982","unstructured":"C.M. Hoffman, M.J. O'Donnel, Programming with equations, ACM TOPLAS, Vol. 4, No. 1, 83\u2013112, 1982.","journal-title":"ACM TOPLAS"},{"key":"21_CR7","unstructured":"J.Hsiang, N.Dershowitz, Rewrite Methods for Clausal and Nonclausal Theorem Proving, Proc. 10th ICALP, July 1983."},{"key":"21_CR8","volume-title":"On Word Problems in Equational Theories","author":"J. Hsiang","year":"1986","unstructured":"J. Hsiang, M. Rusinowitch, On Word Problems in Equational Theories, Computer Science Dept., SUNY at Stony Brook, New York, Aug. 1986 (also in Proc. 14th ICALP, Karlsruhe, July 1987)."},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"G.Huet, J.M.Hullot, Proofs by Induction in Equational Theories with Constructors, Proc. 21st FOCS, 96\u2013107, 1980.","DOI":"10.1109\/SFCS.1980.37"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"J.M.Hullot, Canonical Forms and Unification, Proc. 5\n                  th\n                 CADE, LNCS 87, Springer Verlag, also Tech.Rep. CSL-114, SRI Int'l, April 1980.","DOI":"10.21236\/ADA087640"},{"key":"21_CR11","unstructured":"J.-P.Jouannaud, E.Kounalis, Proofs by induction in equational theories without constructors, Proc. of Logic in Computer Science Conference, Cambridge, MA, June 1986."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"D.Kapur, D.Musser, Proof by Consistency, Artificial Intelligence 31, Feb. 1987.","DOI":"10.1016\/0004-3702(87)90017-8"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"D.Kapur, P.Narendran, H.Zhang, Proof by induction using test sets, Proc. of CADE-8, Oxford, England, July 1986.","DOI":"10.1007\/3-540-16780-3_83"},{"key":"21_CR14","series-title":"Rapport de Recherche","volume-title":"Fair Conditional Term Rewriting Systems: Unification, Termination, and Confluence","author":"S. Kaplan","year":"1983","unstructured":"S. Kaplan, Fair Conditional Term Rewriting Systems: Unification, Termination, and Confluence, Rapport de Recherche, No. 194, Universite de Paris-Sud, Orsay, France, Dec. 1983."},{"key":"21_CR15","series-title":"Technical Report","volume-title":"An equational Approach to Theorem Proving in FOPC","author":"D. Kapur","year":"1984","unstructured":"D. Kapur, P. Narendran, An equational Approach to Theorem Proving in FOPC, Technical Report, GE Corp. Res. and Dev. Center, Schenectady, NY 12345, April 1984."},{"key":"21_CR16","series-title":"Technical Report","volume-title":"On Ground Confluence of Term Rewriting Systems","author":"D. Kapur","year":"1987","unstructured":"D. Kapur, P. Narendran, F. Otto, On Ground Confluence of Term Rewriting Systems, Technical Report 87-06, GE Corp. Res. and Dev. Center, Schenectady, NY 12345, 1987."},{"key":"21_CR17","unstructured":"C.Kirchner, P.Lescanne, Solving Disequations, Proc. 2\n                  nd\n                 IEEE Symp. on Logic in Computer Science, 1987."},{"key":"21_CR18","unstructured":"D.E. Knuth, P.B. Bendix, Simple word problems in Universal Algebras, in J. Leech, Ed., Computational Problems in Abstract Algebras, Pergamon, 1970."},{"key":"21_CR19","volume-title":"Unification Revisited","author":"J-L. Lassez","year":"1986","unstructured":"J-L. Lassez, M.J. Maher, K. Marriott, Unification Revisited, IBM T.J.Watson Research Center, Yorktown Heights, New York, USA, 1986."},{"key":"21_CR20","unstructured":"D.S.Lankford, Canonical Inference, Report ATP-32, Dept. of Math. and Comp. Sci., Univ. of Texas at Austin, Dec. 1975."},{"key":"21_CR21","series-title":"Tech.Rep.","volume-title":"On Proofs in Systems of Equations and Inequations","author":"C. K. Mohan","year":"1987","unstructured":"C.K. Mohan, M.K. Srivas, D. Kapur, On Proofs in Systems of Equations and Inequations, Tech.Rep.87\/02, Computer Science Dept., SUNY at StonyBrook, New York, Jan.1987."},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"C.K.Mohan M.K.Srivas, Function Definitions in Term Rewriting and Applicative Programming, Information and Control, Vol.71, No.3, Academic Press, Dec.1986.","DOI":"10.1016\/S0019-9958(86)80010-9"},{"key":"21_CR23","volume-title":"First International Workshop on Conditional Term Rewriting Systems","author":"C. K. Mohan","year":"1987","unstructured":"C.K. Mohan, M.K. Srivas, Conditional Specifications Using Inequality Assumptions, First International Workshop on Conditional Term Rewriting Systems, Univ. of Paris-Sud, Orsay, France, July 1987."},{"key":"21_CR24","unstructured":"D.R.Musser, Abstract Data Type Specification in the AFFIRM System, Specifications of Reliable Software Conference, Boston, April 1979."},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"D.R.Musser, On Proving Inductive Properties of Abstract Data Types, Proc. 7th POPL, Las Vegas, 1980.","DOI":"10.1145\/567446.567461"},{"key":"21_CR26","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/BF02945004","volume":"2","author":"A. Selman","year":"1972","unstructured":"A. Selman, Completeness of Calculii for Axiomatically Defined classes of Algebras, Algebra Universalis, Vol.2, 20\u201332, 1972.","journal-title":"Algebra Universalis"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"L.Wos, W.McCune, Negative Paramodulation, Eighth Conference on Automated Deduction, Oxford, England, July 1986.","DOI":"10.1007\/3-540-16780-3_93"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"H.Zhang, J.L.Remy, Contextual Rewriting, First Conference on Rewriting Techniques and Applications, Dijon, France, 1985.","DOI":"10.1007\/3-540-15976-2_2"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-18625-5_57","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:46:38Z","timestamp":1558269998000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-18625-5_57"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987]]},"ISBN":["9783540186250","9783540480334"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-18625-5_57","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1987]]},"assertion":[{"value":"27 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}