{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:15:33Z","timestamp":1725455733564},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540605898"},{"type":"electronic","value":"9783540478027"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0015469","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:32:11Z","timestamp":1131863531000},"page":"299-316","source":"Crossref","is-referenced-by-count":3,"title":["Seduct \u2014 A proof compiler for first order logic"],"prefix":"10.1007","author":[{"given":"Karl","family":"Stroetmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"Leo Bachmair. Canonical Equational Proofs. Birkh\u00e4user Boston, Inc., Boston, MA, 1991."},{"key":"17_CR2","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, Orlando, Florida, 1979."},{"issue":"8","key":"17_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"17_CR4","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/S0747-7171(87)80065-2","volume":"4","author":"W. B\u00fcttner","year":"1987","unstructured":"W. B\u00fcttner and H. Simonis. Embedding Boolean expressions into logic programming. Journal of Symbolic Computation, 4:191\u2013205, October 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, chapter 6, pages 243\u2013320. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"17_CR6","volume-title":"Logic for Computer Science","author":"J. Gallier","year":"1986","unstructured":"J. Gallier. Logic for Computer Science. Harper & Row, New York, 1986."},{"key":"17_CR7","volume-title":"A guide to LP, the Larch Prover. Report 82","author":"S. J. Garland","year":"1991","unstructured":"Stephen J. Garland and John V. Guttag. A guide to LP, the Larch Prover. Report 82, DEC Systems Research Center, Palo Alto, CA, December 1991."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Jieh Hsiang and Micha\u00ebl Rusinowitch. On word problems in equational theories. In Thomas Ottmann, editor, Automata, Languages and Programming, volume 267 of Lecture Notes in Computer Science, pages 54\u201371. Springer-Verlag, 1987.","DOI":"10.1007\/3-540-18088-5_6"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"M. Heisel, W. Reif, and W. Stephan. Tactical theorem proving in program verification. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 117\u2013131. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_83"},{"key":"17_CR10","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, Oxford, 1970."},{"key":"17_CR11","volume-title":"Technical report, Siemens AG","author":"C. B. Nielsen","year":"1994","unstructured":"Claus Bendix Nielsen. Boolean unification: a case study in verification with Seduct. Technical report, Siemens AG, Corporate Research and Development, 81730 Munich, Germany, 1994."},{"key":"17_CR12","unstructured":"W. Reif. The Kiv-approach to software verification. This volume."},{"key":"17_CR13","volume-title":"A Guide to Seduct","author":"K. Stroetmann","year":"1994","unstructured":"Karl Stroetmann and Claus Bendix Nielsen. A Guide to Seduct. Siemens AG, Munich, Germany, second edition, 1994.","edition":"second edition"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"R. M. Smullyan. First Order Logic. Springer Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"}],"container-title":["Lecture Notes in Computer Science","KORSO: Methods, Languages, and Tools for the Construction of Correct Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0015469","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T02:28:29Z","timestamp":1554431309000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0015469"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605898","9783540478027"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0015469","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}