{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:26:21Z","timestamp":1725549981296},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540289319"},{"type":"electronic","value":"9783540318224"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11554554_17","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T10:02:57Z","timestamp":1127815377000},"page":"217-230","source":"Crossref","is-referenced-by-count":0,"title":["The Space Efficiency of OSHL"],"prefix":"10.1007","author":[{"given":"Swaha","family":"Miller","sequence":"first","affiliation":[]},{"given":"David A.","family":"Plaisted","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"17_CR1","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D.A. Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. Journal of Automated Reasoning\u00a025(3), 167\u2013217 (2000)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"17_CR2","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1023\/A:1020512924736","volume":"29","author":"A. Yahya","year":"2002","unstructured":"Yahya, A., Plaisted, D.A.: Ordered semantic hyper tableaux. Journal of Automated Reasoning\u00a029(1), 17\u201357 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/3-540-45744-5_30","volume-title":"Automated Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: DCTP: A Disconnection Calculus Theorem Prover. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol.\u00a02083, pp. 381\u2013385. Springer, Heidelberg (2001)"},{"issue":"2","key":"17_CR4","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1.. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR5","unstructured":"Das, S., Plaisted, D.A.: An improved propositional approach to first-order theorem proving. In: Workshop on Model Computation - Principles, Algorithms, Applications at The 19th International Conference on Automated Deduction (2003)"},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012, 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"issue":"2","key":"17_CR7","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"Loveland, D.W.: Mechanical theorem-proving by model elimination. Journal of the ACM\u00a015(2), 236\u2013251 (1968)","journal-title":"Journal of the ACM"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/10721959_16","volume-title":"Automated Deduction - CADE-17","author":"P. Baumgartner","year":"2000","unstructured":"Baumgartner, P.: FDPLL \u2013 A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 200\u2013219. Springer, Heidelberg (2000)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: A Theorem Prover Implemented in Prolog. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 415\u2013434. Springer, Heidelberg (1988)"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"P.C. Gilmore","year":"1960","unstructured":"Gilmore, P.C.: A proof method for quantification theory. IBM Journal of Research and Development\u00a04, 28\u201335 (1960)","journal-title":"IBM Journal of Research and Development"},{"key":"17_CR11","first-page":"25","volume":"9","author":"D.A. Plaisted","year":"1992","unstructured":"Plaisted, D.A., Lee, S.J.: Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning\u00a09, 25\u201342 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: Otter 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, Illinois (1994)","DOI":"10.2172\/10129052"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C. Weidenbach","year":"1997","unstructured":"Weidenbach, C.: SPASS version 0.49. Journal of Automated Reasoning\u00a018, 247\u2013252 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR14","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf. Journal of Automated Reasoning\u00a018, 199\u2013204 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR15","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, 183\u2013212 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-48660-7_20","volume-title":"Automated Deduction - CADE-16","author":"T. Hillenbrand","year":"1999","unstructured":"Hillenbrand, T., Jaeger, A., L\u00f6chner, B.: Waldmeister - Improvements in Performance and Ease of Use. In: Ganzinger, H. (ed.) CADE 1999. LNCS, vol.\u00a01632, pp. 232\u2013236. Springer, Heidelberg (1999)"},{"key":"17_CR17","first-page":"341","volume-title":"Proceedings of the 12th Florida Artificial Intelligence Research Symposium","author":"G. Sutcliffe","year":"1999","unstructured":"Sutcliffe, G., Seyfang, D.: Smart Selective Competition Parallelism ATP. In: Kumar, A., Russell, I. (eds.) Proceedings of the 12th Florida Artificial Intelligence Research Symposium, pp. 341\u2013345. AAAI Press, Menlo Park (1999)"},{"key":"17_CR18","first-page":"346","volume-title":"Proceedings of the 12th Florida Artificial Intelligence Research Symposium","author":"G. Stenz","year":"1999","unstructured":"Stenz, G., Wolf, A.: Strategy Selection by Genetic Programming. In: Kumar, A., Russell, I. (eds.) Proceedings of the 12th Florida Artificial Intelligence Research Symposium, pp. 346\u2013350. AAAI Press, Menlo Park (1999)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-46508-1_5","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"D.A. Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Replacement rules with definition detection. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS, vol.\u00a01761, pp. 80\u201394. Springer, Heidelberg (2000) (Invited paper)"},{"key":"17_CR20","unstructured":"Zhu, Y., Plaisted, D.A.: FOLPLAN: A Semantically Guided First-Order Planner. In: 10th International FLAIRS Conference (1997)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11554554_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:34:46Z","timestamp":1558272886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11554554_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540289319","9783540318224"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11554554_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}