{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:57:44Z","timestamp":1725663464021},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540510819"},{"type":"electronic","value":"9783540461494"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-51081-8_135","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:38:17Z","timestamp":1330184297000},"page":"548-550","source":"Crossref","is-referenced-by-count":2,"title":["KBlab: An equational theorem prover for the Macintosh"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[]},{"given":"Giancarlo","family":"Sanna","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"41_CR1","unstructured":"L.Bachmair, N.Dershowitz, J.Hsiang \u2014 Orderings for Equational Proofs In Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, 346\u2013357, Cambridge, MA, June 1986"},{"key":"41_CR2","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0304-3975(85)90011-8","volume":"35","author":"L. Fribourg","year":"1985","unstructured":"L. Fribourg \u2014 A superposition oriented theorem prover J. of Theoretical Computer Science, Vol. 35, 129\u2013164, 1985","journal-title":"J. of Theoretical Computer Science"},{"key":"41_CR3","doi-asserted-by":"crossref","unstructured":"L.Fribourg \u2014 A Strong Restriction to The Inductive Completion Procedure In Proceedings 13th Int. Conf. on Automata, Languages and Programming, Rennes, France, July 1986, Lecture Notes in Computer Science 226, 1986","DOI":"10.1007\/3-540-16761-7_60"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Glickfield, R.Overbeek \u2014 A Foray Into Combinatory Logic J. of Automated Reasoning, Vol. 2, No. 4, Dec. 1986","DOI":"10.1007\/BF00248251"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"J.Hsiang, M.Rusinowitch \u2014 On Word Problems in Equational Theories In Th.Ottman ed., Proceedings 14th Int. Conf. on Automata, Languages and Programming, Karlsrhue, W.Germany, July 1987, Lecture Notes in Computer Science 267, 1987","DOI":"10.1007\/3-540-18088-5_6"},{"key":"41_CR6","unstructured":"J.Hsiang, J.Mzali \u2014 SbREVE User's Guide To appear as Technical Report L.R.I. Universit\u00e8 de Paris Sud, Orsay, France"},{"key":"41_CR7","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"G. Huet \u2014 A Complete Proof of Correctness of Knuth-Bendix Completion Algorithm J. of Computer and System Sciences, Vol. 23, 11\u201321, 1981","journal-title":"J. of Computer and System Sciences"},{"key":"41_CR8","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"G. Huet, J.M. Hullot \u2014 Proofs by Induction in Equational Theories with Constructors J. of Computer and System Sciences, Vol. 25, 239\u2013266, 1982","journal-title":"J. of Computer and System Sciences"},{"key":"41_CR9","first-page":"263","volume-title":"Simple Word Problems in Universal Algebras","author":"D.E. Knuth","year":"1970","unstructured":"D.E. Knuth, P. Bendix \u2014 Simple Word Problems in Universal Algebras In J. Leech ed., Proceedings of the Conf. on Computational Problems in Abstract Algebras, Oxford, 1967, Pergamon Press, Oxford, 263\u2013298, 1970"},{"key":"41_CR10","unstructured":"B.McCune, L.Wos \u2014 Some Fixed Points Problems in Combinatory Logic AAR Newsletter"},{"key":"41_CR11","unstructured":"A.Ohsuga, K.Sakai \u2014 Refutational Theorem Proving for Equational Systems Based on Term Rewriting Technical Report COMP86-40, ICOT, 1986"},{"key":"41_CR12","volume-title":"How to mock a mocking bird","author":"R. Smullyan","year":"1985","unstructured":"R. Smullyan \u2014 How to mock a mocking bird Alfred A. Knopf, New York 1985"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-51081-8_135.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:19:32Z","timestamp":1605629972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-51081-8_135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540510819","9783540461494"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-51081-8_135","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]}}}