{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T11:33:42Z","timestamp":1742988822740,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668220"},{"type":"electronic","value":"9783540466956"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46695-9_21","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T08:37:07Z","timestamp":1186907827000},"page":"244-254","source":"Crossref","is-referenced-by-count":1,"title":["PTTP+GLiDeS: Guiding Linear Deductions with Semantics"],"prefix":"10.1007","author":[{"given":"Marianne","family":"Brown","sequence":"first","affiliation":[]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"A. Bundy. The Computer Modelling of Mathematical Reasoning. Academic Press, 1983."},{"key":"21_CR2","volume-title":"CLIN-S User\u2019s Manual","author":"H. Chu","year":"1994","unstructured":"H. Chu. CLIN-S User\u2019s Manual. Chapel Hill, USA, 1994."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"D.A. de Waal and J.P. Gallagher. The Applicability of Logic Programming Analysis and Transformation to Theorem Proving. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, number 814 in Lecture Notes in Artificial Intelligence, pages 207\u2013221. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_15"},{"issue":"2","key":"21_CR4","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"D.W. Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the ACM, 15(2):236\u2013251, 1968.","journal-title":"Journal of the ACM"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"D.W. Loveland. A Linear Format for Resolution. In Laudet M. et al., editor, Proceedings of the IRIA Symposium on Automatic Demonstration, pages 147\u2013162. Springer-Verlag, 1970.","DOI":"10.1007\/BFb0060630"},{"key":"21_CR6","first-page":"95","volume":"3","author":"D. Luckham","year":"1968","unstructured":"D. Luckham. Some Tree-paring Strategies for Theorem Proving. Machine Intelligence, 3:95\u2013112, 1968.","journal-title":"Machine Intelligence"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"D. Luckham. Refinement Theorems in Resolution Theory. In Laudet M. et al., editor, Proceedings of the Symposium on Automatic Demonstration, pages 163\u2013190. Springer-Verlag, 1970.","DOI":"10.1007\/BFb0060631"},{"key":"21_CR8","series-title":"Technical Report Technical Report","volume-title":"A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems","author":"W.W. McCune","year":"1994","unstructured":"W.W. McCune. A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems. Technical Report Technical Report ANL\/MCS-TM-194, Argonne National Laboratory, Argonne, USA, 1994."},{"issue":"1","key":"21_CR9","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1):23\u201341, January 1965.","journal-title":"Journal of the ACM"},{"key":"21_CR10","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J.R. Slagle","year":"1967","unstructured":"J.R. Slagle. Automatic Theorem Proving with Renamable and Sematic Resolution. Journal of the ACM, 14:687\u2013697, October 1967.","journal-title":"Journal of the ACM"},{"key":"21_CR11","unstructured":"J.K. Slaney. SCOTT: A Model-Guided Theorem Prover. In R. Bajcsy, editor, Proceedings of the 13th International Conference on Artificial Intelligence, pages 109\u2013114. Morgan-Kaufman, 1993."},{"key":"21_CR12","unstructured":"M.E. Stickel. A Prolog Technology Theorem Prover. In Proceedings of the 1st International Symposium on Logic Programming, pages 211\u2013217. IEEE Computer Society Press, 1984."},{"key":"21_CR13","series-title":"Technical Report Technical Note","volume-title":"A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog","author":"M.E. Stickel","year":"1989","unstructured":"M.E. Stickel. A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. Technical Report Technical Note 464, SRI International, Menlo Park, USA, 1989."},{"key":"21_CR14","series-title":"Lecture Notes in Artifical Intelligence","first-page":"268","volume-title":"Proceedings of the 11th International Conference on Automated Deduction","author":"G. Sutcliffe","year":"1992","unstructured":"G. Sutcliffe. Linear-Input Subset Analysis. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, number 607 in Lecture Notes in Artifical Intelligence, pages 268\u2013280, Saratoga Springs, NY, USA, June 1992. Springer-Verlag."},{"issue":"2","key":"21_CR15","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"G. Sutcliffe and C.B. Suttner. The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning, 21(2):177\u2013203, 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"21_CR16","unstructured":"L. Wos. Automated Reasoning-33 Basic Research Problems. Prentice-Hall, 1988."},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"L. Wos, D. Carson, and G.A. Robinson. The Unit Preference Strategy in Theorem Proving. In Proceedings of the AFIPS 1964 Fall Joint Computer Conference, pages 615\u2013621. Spartan Books, 1964.","DOI":"10.1145\/1464052.1464109"},{"key":"21_CR18","volume-title":"Automated Reasoning Introduction and Applications","author":"L. Wos","year":"1984","unstructured":"L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning Introduction and Applications. Prentice-Hall, Englewood Cliffs, New Jersey, 1984."}],"container-title":["Lecture Notes in Computer Science","Advanced Topics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46695-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T01:06:22Z","timestamp":1732842382000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-46695-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668220","9783540466956"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-46695-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}