{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:49:48Z","timestamp":1725475788902},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_32","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"411-416","source":"Crossref","is-referenced-by-count":1,"title":["System Description: PTTP+GLiDeS Semantically Guided PTTP"],"prefix":"10.1007","author":[{"given":"Marianne","family":"Brown","sequence":"first","affiliation":[]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-46695-9_21","volume-title":"Advanced Topics in Artificial Intelligence","author":"M. Brown","year":"1999","unstructured":"Brown, M., Sutcliffe, G.: PTTP+GLiDeS: Guiding Linear Deductions with Semantics. In: Foo, N.Y. (ed.) AI 1999. LNCS (LNAI), vol.\u00a01747, pp. 244\u2013254. Springer, Heidelberg (1999)"},{"key":"32_CR2","first-page":"328","volume-title":"Proceedings of the 14th International Joint Conference on Artificial Intelligence","author":"R. Caferra","year":"1995","unstructured":"Caferra, R., Peltier, N.: Extending Semantic Resolution via Automated Model Building: Applications. In: Mellish, C.S. (ed.) Proceedings of the 14th International Joint Conference on Artificial Intelligence, pp. 328\u2013334. Morgan Kaufmann, San Francisco (1995)"},{"key":"32_CR3","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/3-540-58156-1_14","volume-title":"Automated Deduction - CADE-12","author":"H. Chu","year":"1994","unstructured":"Chu, H., Plaisted, D.: Semantically Guided First-order Theorem Proving using Hyper-linking. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 192\u2013206. Springer, Heidelberg (1994)"},{"key":"32_CR4","series-title":"LNAI","first-page":"207","volume-title":"Automated Deduction - CADE-12","author":"D.A. Waal de","year":"1994","unstructured":"de Waal, D.A., Gallagher, J.P.: The Applicability of Logic Programming Analysis and Transformation to Theorem Proving. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 207\u2013221. Springer, Heidelberg (1994)"},{"issue":"2","key":"32_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning\u00a08(2), 183\u2013212 (1992)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"32_CR6","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D.W. Loveland","year":"1969","unstructured":"Loveland, D.W.: A Simplified Format for the Model Elimination Theorem-Proving Procedure. Journal of the ACM\u00a016(3), 349\u2013363 (1969)","journal-title":"Journal of the ACM"},{"key":"32_CR7","unstructured":"McCune, W.W.: 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)"},{"key":"32_CR8","first-page":"109","volume-title":"Proceedings of the 13th International Conference on Artificial Intelligence","author":"J.K. Slaney","year":"1993","unstructured":"Slaney, J.K.: SCOTT: A Model-Guided Theorem Prover. In: Bajcsy, R. (ed.) Proceedings of the 13th International Conference on Artificial Intelligence, pp. 109\u2013114. Morgan-Kaufman, San Francisco (1993)"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Stickel, M.E.: A Prolog Technology Theorem Prover: A New Exposition and Im- plementation in Prolog. Technical Report Technical Note 464, SRI International, Menlo Park, USA (1989)","DOI":"10.1007\/3-540-52531-9_135"},{"key":"32_CR10","series-title":"LNAI","first-page":"268","volume-title":"Automated Deduction - CADE-11","author":"G. Sutcliffe","year":"1992","unstructured":"Sutcliffe, G.: Linear-Input Subset Analysis. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 268\u2013280. Springer, Heidelberg (1992)"},{"key":"32_CR11","series-title":"LNAI","first-page":"677","volume-title":"Automated Deduction - CADE-11","author":"G. Sutcliffe","year":"1992","unstructured":"Sutcliffe, G.: The Semantically Guided Linear Deduction System. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 677\u2013680. Springer, Heidelberg (1992)"},{"issue":"2","key":"32_CR12","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:42:31Z","timestamp":1556019751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/10721959_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}