{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,26]],"date-time":"2023-09-26T12:50:04Z","timestamp":1695732604663},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,3,3]],"date-time":"2012-03-03T00:00:00Z","timestamp":1330732800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,1]]},"DOI":"10.1007\/s10817-012-9245-6","type":"journal-article","created":{"date-parts":[[2012,3,3]],"date-time":"2012-03-03T19:28:01Z","timestamp":1330802881000},"page":"99-117","source":"Crossref","is-referenced-by-count":5,"title":["Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions"],"prefix":"10.1007","volume":"50","author":[{"given":"James P.","family":"Bridge","sequence":"first","affiliation":[]},{"given":"Lawrence Charles","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,3,3]]},"reference":[{"issue":"3","key":"9245_CR1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.: MetiTarski: An automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010). doi: 10.1007\/s10817-009-9149-2","journal-title":"J. Autom. Reason."},{"key":"9245_CR2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning, chap. 2","author":"L Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 2, pp. 19\u201399. Elsevier, Amsterdam (2001)"},{"key":"9245_CR3","first-page":"93","volume-title":"Formal Methods in Computer Aided Design","author":"W Denman","year":"2009","unstructured":"Denman, W., Akbarpour, B., Tahar, S., Zaki, M., Paulson, L.C.: Formal verification of analog designs using MetiTarski. In: Biere, A., Pixley, C. (eds.) Formal Methods in Computer Aided Design, pp. 93\u2013100. IEEE, Piscataway (2009). doi: 10.1109\/FMCAD.2009.5351136"},{"key":"9245_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10472-009-9150-9","volume":"55","author":"A Fietzke","year":"2009","unstructured":"Fietzke, A., Weidenbach, C.: Labelled splitting. Ann. Math. Artif. Intell. 55, 3\u201334 (2009). doi: 10.1007\/s10472-009-9150-9","journal-title":"Ann. Math. Artif. Intell."},{"key":"9245_CR5","unstructured":"Hurd, J.: Metis first order prover (2007). URL:\u00a0 http:\/\/gilith.com\/software\/metis\/"},{"issue":"2","key":"9245_CR6","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W McCune","year":"1997","unstructured":"McCune, W., Wos, L.: Otter: The CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211\u2013220 (1997). doi: 10.1023\/A:1005843632307","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9245_CR7","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41\u201357 (2009). doi: 10.1016\/j.jal.2007.07.004","journal-title":"J. Appl. Log."},{"key":"9245_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-99970-3","volume-title":"Analytic Inequalities","author":"DS Mitrinovi\u0107","year":"1970","unstructured":"Mitrinovi\u0107, D.S., Vasi\u0107, P.M.: Analytic Inequalities. Springer, New York (1970)"},{"key":"9245_CR9","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-45653-8_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning: 8th International Conference, LPAR, LNCS 2250","author":"H Nivelle","year":"2001","unstructured":"Nivelle, H.: Splitting through new proposition symbols. In: Nieuwenhuis, R., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning: 8th International Conference, LPAR, LNCS 2250, pp. 172\u2013185. Springer, New York (2001). doi: 10.1007\/3-540-45653-8_12","edition":"2250"},{"key":"9245_CR10","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning, chap. 6","author":"A Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 6, pp. 335\u2013367. Elsevier, Amsterdam (2001)"},{"key":"9245_CR11","unstructured":"Riazanov, A., Voronkov, A.: Splitting without backtracking. In: International Joint Conference on Artificial Intelligence (IJCAI-17), vol. 1, pp. 611\u2013617 (2001). http:\/\/www.cs.man.ac.uk\/~voronkov\/papers\/ijcai01.ps"},{"key":"9245_CR12","first-page":"201","volume-title":"Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, no. 112 in Frontiers in Artificial Intelligence and Applications","author":"G Sutcliffe","year":"2004","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, no. 112 in Frontiers in Artificial Intelligence and Applications, pp. 201\u2013215. IOS Press, Amsterdam (2004)"},{"key":"9245_CR13","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C Weidenbach","year":"1997","unstructured":"Weidenbach, C.: SPASS - version 0.49. J. Autom. Reason. 18, 247\u2013252 (1997). doi: 10.1023\/A:1005812220011","journal-title":"J. Autom. Reason."},{"key":"9245_CR14","doi-asserted-by":"crossref","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning, chap. 27","author":"C Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 27, pp. 1965\u20132013. Elsevier, Amsterdam (2001)"},{"issue":"4","key":"9245_CR15","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L Wos","year":"1965","unstructured":"Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12(4), 536\u2013541 (1965). doi: 10.1145\/321296.321302","journal-title":"J. ACM"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9245-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9245-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9245-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:51Z","timestamp":1559251311000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9245-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,3]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["9245"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9245-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,3]]}}}