{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:57:32Z","timestamp":1725857852363},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_25","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T08:54:04Z","timestamp":1465635244000},"page":"362-370","source":"Crossref","is-referenced-by-count":7,"title":["Effective Normalization Techniques for HOL"],"prefix":"10.1007","author":[{"given":"Max","family":"Wisniewski","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Steen","sequence":"additional","affiliation":[]},{"given":"Kim","family":"Kern","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"25_CR1","volume-title":"The Stanford Encyclopedia of Philosophy","author":"P Andrews","year":"2014","unstructured":"Andrews, P.: Church\u2019s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Stanford University, Spring (2014)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"25_CR3","series-title":"Mathematical Logic and Foundations","first-page":"171","volume-title":"All about Proofs, Proof for All","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C.: Higher-order automated theorem provers. In: Delahaye, D., Woltzenlogel Paleo, B. (eds.) All about Proofs, Proof for All. Mathematical Logic and Foundations, pp. 171\u2013214. College Publications, London (2015)"},{"issue":"1:6","key":"25_CR4","first-page":"1","volume":"5","author":"C Benzm\u00fcller","year":"2009","unstructured":"Benzm\u00fcller, C., Brown, C., Kohlhase, M.: Cut-simulation, impredicativity. Log. Methods Comput. Sci. 5(1:6), 1\u201321 (2009)","journal-title":"Log. Methods Comput. Sci."},{"issue":"4","key":"25_CR5","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/s10817-015-9348-y","volume":"55","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Sultana, N., Thei\u00df, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389\u2013404 (2015)","journal-title":"J. Autom. Reason."},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012)"},{"key":"25_CR8","unstructured":"Kern, K.: Improved computation of CNF in higher-order logics. Bachelor thesis, Freie Universit\u00e4t Berlin (2015)"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Niles, I., Pease, A.: Towards a standard upper ontology. In: Proceedings of the International Conference on Formal Ontology in Information Systems, pp. 2\u20139. ACM (2001)","DOI":"10.1145\/505168.505170"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/BFb0054274","volume-title":"Automated Deduction - CADE-15","author":"A Nonnengart","year":"1998","unstructured":"Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 397\u2013411. Springer, Heidelberg (1998)"},{"key":"25_CR12","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning","author":"A Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 335\u2013367. Gulf Professional Publishing, Houston (2001)"},{"issue":"3","key":"25_CR13","first-page":"73","volume":"5","author":"LC Paulson","year":"1999","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with isabelle. J. Univers. Comput. Sci. 5(3), 73\u201387 (1999)","journal-title":"J. Univers. Comput. Sci."},{"issue":"4","key":"25_CR14","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"25_CR15","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1\u201327 (2010)","journal-title":"J. Formaliz. Reason."},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-61511-3_75","volume-title":"Automated Deduction \u2014 Cade-13","author":"C Weidenbach","year":"1996","unstructured":"Weidenbach, C., Gaede, B., Rock, G.: SPASS & FLOTTER version 0.42. In: McRobbie, M.A., Slaney, J.K. (eds.) Cade-13. LNCS, vol. 1104, pp. 141\u2013145. Springer, Heidelberg (1996)"},{"key":"25_CR17","unstructured":"Wisniewski, M., Steen, A., Benzm\u00fcller, C.: The Leo-III project. In: Bolotov, A., Kerber, M. (eds.) Joint Automated Reasoning Workshop and Deduktionstreffen, p. 38 (2014)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:12:44Z","timestamp":1498306364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}