{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:17Z","timestamp":1725663497149},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540563938"},{"type":"electronic","value":"9783540475491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56393-8_18","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:07:07Z","timestamp":1330254427000},"page":"242-256","source":"Crossref","is-referenced-by-count":5,"title":["Reduction techniques for first-order reasoning"],"prefix":"10.1007","author":[{"given":"Francois","family":"Bronsard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uday S.","family":"Reddy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Comp. Science, Vol 355","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/3-540-51081-8_97","volume-title":"Rewriting Techniques and Applications","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair. Proof normalization for resolution and paramodulation. In N. Dershowitz, editor, Rewriting Techniques and Applications, pages 15\u201328. Springer-Verlag, Berlin, 1989. (Lecture Notes in Comp. Science, Vol 355)."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Harald Ganzinger. Completion of first order clauses with equality. In S. Kaplan and M. Okada, editors, Conditional and Typed Rewriting Systems \u2014 Second International CTRS Workshop, pages 162\u2013180. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54317-1_89"},{"key":"18_CR3","first-page":"2","volume-title":"Conditional and Typed Rewriting Systems \u2014 Second International CTRS Workshop","author":"F. Bronsard","year":"1991","unstructured":"F. Bronsard and U. S. Reddy. Conditional rewriting in Focus. In S. Kaplan and M. Okada, editors, Conditional and Typed Rewriting Systems \u2014 Second International CTRS Workshop, pages 2\u201313. Springer-Verlag, Berlin, 1991."},{"key":"18_CR4","first-page":"243","volume-title":"Handbook of Theoretical Computer Science B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243\u2013320. North-Holland, Amsterdam, 1990."},{"key":"18_CR5","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(08)80132-0","volume":"11","author":"H. Ganzinger","year":"1991","unstructured":"H. Ganzinger. A completion procedure for conditional equations. J. Symbolic Computation, 11:51\u201381, 1991.","journal-title":"J. Symbolic Computation"},{"key":"18_CR6","first-page":"141","volume-title":"Vol. 230 of Lecture Notes in Computer Science","author":"J. Hsiang","year":"1986","unstructured":"Jieh Hsiang and Micha\u00ebl Rusinowitch. A new method for establishing refutational completeness in theorem proving. In J. H. Siekmann, editor, Proceedings of the Eighth International Conference on Automated Deduction, pages 141\u2013152, Oxford, England, July 1986. Vol. 230 of Lecture Notes in Computer Science, Springer, Berlin."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and F. Orejas. Clausal rewriting. In S. Kaplan and M. Okada, editors, Conditional and Typed Rewriting Systems \u2014 Second International CTRS Workshop, pages 246\u2013258. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54317-1_95"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"H. Zhang and D. Kapur. First-order theorem proving using conditional rewrite rules. In E. Lusk and R. Overbeek, editors, 9th Intern. Conf. on Automated Deduction, pages 1\u201320. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012820"}],"container-title":["Lecture Notes in Computer Science","Conditional Term Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56393-8_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:03:33Z","timestamp":1605647013000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56393-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540563938","9783540475491"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-56393-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}