{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T15:43:27Z","timestamp":1746114207836},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540100096"},{"type":"electronic","value":"9783540381402"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1980]]},"DOI":"10.1007\/3-540-10009-1_19","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T12:03:02Z","timestamp":1330171382000},"page":"232-249","source":"Crossref","is-referenced-by-count":7,"title":["Data structures and control architecture for implementation of theorem-proving programs"],"prefix":"10.1007","author":[{"given":"Ross A.","family":"Overbeek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ewing L.","family":"Lusk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,25]]},"reference":[{"key":"19_CR1","unstructured":"E. Lusk and R. Overbeek, Experiments with Resolution-Based Theorem-Proving Algorithms, Comp. Math. with Appls, to appear."},{"key":"19_CR2","unstructured":"E. Lusk, and R. Overbeek, Experiments with Resolution-Based Theorem-Proving Algorithms (extend abstract), Third Workshop on Automated Deduction, Boston, 1977."},{"key":"19_CR3","first-page":"1","volume":"2","author":"J. D. McCharen","year":"1976","unstructured":"J. D. McCharen, R. A. Overbeek, and L. Wos, Complexity and related enhancements for automated theorem proving programs, Comp. Maths. with Appls., 2, 1\u201316 (1976).","journal-title":"Comp. Maths. with Appls."},{"issue":"8","key":"19_CR4","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. D. McCharen","year":"1976","unstructured":"J. D. McCharen, R. A. Overbeek, and L. Wos, Problems and Experiments for and with automated theorem-proving programs, IEEE Trans. on Computers, C-25, No. 8, 773\u2013782, (1976).","journal-title":"IEEE Trans. on Computers"},{"key":"19_CR5","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/321812.321814","volume":"21","author":"R. A. Overbeek","year":"1974","unstructured":"R. A. Overbeek, A New class of automated theorem-proving algorithms, JACM, 21, 191\u2013200 (1974).","journal-title":"JACM"},{"key":"19_CR6","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0898-1221(75)90019-X","volume":"1","author":"R. A. Overbeek","year":"1975","unstructured":"R. A. Overbeek, An implementation of hyper-resolution, Comp. Maths. with Appls., 1, 201\u2013214 (1975).","journal-title":"Comp. Maths. with Appls."},{"key":"19_CR7","unstructured":"J. A. Robinson, Mechanizing higher-order logic, Mach. Intelligence 4, Amer. Elsevier Pub. Co., Inc., 151\u2013170 (1969)."},{"key":"19_CR8","unstructured":"S. Winker and L. Wos, Automated Generation of Models and Computer Examples and its Application to Open Questions in Ternary Boolean Algebra, Proc. Eighth Int. Symposium on Multiple-Valued Logic, pp. 251\u2013256. Rosemont, Illinois (1978); IEEE (1978)"},{"key":"19_CR9","unstructured":"S. Winker, L. Wos, and E. Lusk, Semigroups, involutions, and antiantomorphisms: a computer solution to an open question, in preparation."},{"key":"19_CR10","unstructured":"S. Winker, Generation and verification of finite models and counterexamples using an automated theorem prover, answering two open questions, Proceedings of the Fourth Workshop on Automated Deduction, Austin, 1979."},{"key":"19_CR11","unstructured":"L. Wos, S. Winker, and L. Henschen, Hyperparamodulation: a refinement of paramodulation, in preparation."},{"key":"19_CR12","unstructured":"W. Wojcieckowski and A. Wojcik, Multiple-valued logic design by theorem proving, Proceedings of the Ninth International Symposium on Multiple-Valued Logic, Bathe, England, May 1979."}],"container-title":["Lecture Notes in Computer Science","5th Conference on Automated Deduction Les Arcs, France, July 8\u201311, 1980"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-10009-1_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T16:33:28Z","timestamp":1619541208000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-10009-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1980]]},"ISBN":["9783540100096","9783540381402"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-10009-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1980]]}}}