{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:48:57Z","timestamp":1767926937217,"version":"3.49.0"},"reference-count":88,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,7,12]],"date-time":"2015-07-12T00:00:00Z","timestamp":1436659200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["NI 491\/14-1"],"award-info":[{"award-number":["NI 491\/14-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,2]]},"DOI":"10.1007\/s10817-015-9335-3","type":"journal-article","created":{"date-parts":[[2015,7,11]],"date-time":"2015-07-11T06:16:33Z","timestamp":1436595393000},"page":"155-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Semi-intelligible Isar Proofs from Machine-Generated Proofs"],"prefix":"10.1007","volume":"56","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sascha","family":"B\u00f6hme","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias","family":"Fleury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steffen Juilf","family":"Smolka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert","family":"Steckermeier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,12]]},"reference":[{"key":"9335_CR1","doi-asserted-by":"crossref","unstructured":"Alama, J.: Escape to Mizar from ATPs. In: Fontaine, P., Schmidt, R., Schulz, S. (eds.) PAAR-2012, EPiC, vol. 21, pp 3\u201311. EasyChair (2013)","DOI":"10.29007\/s1ts"},{"key":"9335_CR2","doi-asserted-by":"crossref","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) CPP 2011, LNCS, vol. 7086, pp 135\u2013150. Springer (2011)","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"9335_CR3","doi-asserted-by":"crossref","unstructured":"Autexier, S., Benzm\u00fcller, C., Fiedler, A., Horacek, H., Vo, Q.B.: Assertion-level proof representation with under-specification. Electr. Notes Theor. Comput. Sci. 93, 5\u201323 (2004)","DOI":"10.1016\/j.entcs.2003.12.026"},{"key":"9335_CR4","doi-asserted-by":"crossref","unstructured":"Azmy, N., Weidenbach, C.: Computing tiny clause normal forms. In: Bonacina, M.P. (ed.) CADE-24, LNCS, vol. 7898, pp 109\u2013125. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_7"},{"key":"9335_CR5","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp 19\u201399. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"9335_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, LNCS, vol. 6806, pp 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9335_CR7","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard\u2014Version 2.0. In: Gupta, A., Kroening, D. (eds.) SMT 2010 (2010)"},{"key":"9335_CR8","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II\u2014A cooperative automatic theorem prover for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008, LNCS, vol. 5195, pp 162\u2013170. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"9335_CR9","unstructured":"Besson, F., Fontaine, P., Th\u00e9ry, L.: A flexible proof format for SMT: A proposal. In: Fontaine, P., Stump, A. (eds.) PxTP 2011, pp 15\u201326 (2011)"},{"key":"9335_CR10","unstructured":"Blanchette, J.C.: Automatic proofs and refutations for higher-order logic. Ph.D. thesis, Dept. of Informatics, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"key":"9335_CR11","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C.: Redirecting proofs by contradiction. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EPiC, vol. 14, pp 11\u201326. EasyChair (2013)","DOI":"10.29007\/wm8b"},{"issue":"1","key":"9335_CR12","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reason."},{"key":"9335_CR13","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S. (eds.) TACAS 2013, LNCS, vol. 7795, pp 493\u2013507. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_34"},{"key":"9335_CR14","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle\u2014Superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A. (eds.) ITP 2012, LNCS, vol. 7406, pp 345\u2013360. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8_24"},{"key":"9335_CR15","unstructured":"B\u00f6hme, S.: Proving theorems of higher-order logic with SMT solvers. Ph.D. thesis, Dept. of Informatics, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"key":"9335_CR16","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010, LNCS, vol. 6173, pp 107\u2013121. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"9335_CR17","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L. (eds.) ITP 2010, LNCS, vol. 6172, pp 179\u2013194. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"9335_CR18","doi-asserted-by":"crossref","unstructured":"Bouton, T, de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22, LNCS, vol. 5663, pp 151\u2013156. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"9335_CR19","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"AR Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Form. Asp. Comput. 20, 379\u2013405 (2008)","journal-title":"Form. Asp. Comput."},{"key":"9335_CR20","doi-asserted-by":"crossref","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 (2012)","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"9335_CR21","unstructured":"Brown, C.E.: Using Satallax to generate proof terms for conjectures in Coq. Presentation at AIPA 2012 (2012)"},{"key":"9335_CR22","unstructured":"Caminati, M.: Re: [isabelle] sledgehammer, smt and metis. https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2014-November\/msg00128.html (2014)"},{"key":"9335_CR23","doi-asserted-by":"crossref","unstructured":"Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for Presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005, LNCS, vol. 3835, pp 367\u2013380. Springer (2005)","DOI":"10.1007\/11591191_26"},{"issue":"2","key":"9335_CR24","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"issue":"2","key":"9335_CR25","doi-asserted-by":"crossref","first-page":"526","DOI":"10.1006\/jabr.1998.7467","volume":"208","author":"BI Dahn","year":"1998","unstructured":"Dahn, B.I.: Robbins algebras are Boolean: a revision of McCune\u2019s computer-generated solution of Robbins problem. J. Algebra 208(2), 526\u2013532 (1998)","journal-title":"J. Algebra"},{"key":"9335_CR26","unstructured":"Davis, M.: Obvious logical inferences. In: Hayes, P.J. (ed.) IJCAI \u201981, pp 530\u2013531. William Kaufmann (1981)"},{"key":"9335_CR27","unstructured":"Diekmann, C.: Network security policy verification. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http:\/\/afp.sf.net\/entries\/Network_Security_Policy_Verification.shtml (2014)"},{"key":"9335_CR28","unstructured":"Fleury, M.: Translation of proofs provided by external provers. Internship report, Technische Universit\u00e4t M\u00fcnchen. http:\/\/perso.eleves.ens-rennes.fr\/~mfleur01\/documents\/Fleury_internship2014.pdf (2014)"},{"key":"9335_CR29","unstructured":"Foster, S., Struth, G.: Regular algebras. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http:\/\/afp.sf.net\/entries\/Network_Security_Policy_Verification.shtml (2014)"},{"key":"9335_CR30","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Math. Z. 39, 176\u2013210 (1935)","journal-title":"Math. Z."},{"key":"9335_CR31","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press (1993)"},{"key":"9335_CR32","unstructured":"Herbrand, J.: Th\u00e8ses pr\u00e9sent\u00e9es \u00e0 la facult\u00e9 des sciences de paris pour obtenir le grade de docteur \u00e8s sciences math\u00e9matiques. Ph.D. thesis, Science Faculty, Universit\u00e9 de Paris (1930)"},{"issue":"2","key":"9335_CR33","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T Hillenbrand","year":"1997","unstructured":"Hillenbrand, T., Buch, A., Vogt, R., L\u00f6chner, B.: WALDMEISTER\u2014High-performance equational deduction. J. Autom. Reason. 18(2), 265\u2013270 (1997)","journal-title":"J. Autom. Reason."},{"key":"9335_CR34","unstructured":"Hoder, K., Kovacs, L., Voronkov, A.: Vampire usage and demo. Presentation at the Vampire tutorial at CADE-23. http:\/\/www.complang.tuwien.ac.at\/lkovacs\/Cade23_Tutorial_Slides\/Session2_Slides.pdf (2011)"},{"key":"9335_CR35","doi-asserted-by":"crossref","unstructured":"Huang, X.: Translating machine-generated resolution proofs into ND-proofs at the assertion level. In: Foo, N.Y., Goebel, R. (eds.) PRICAI \u201996, LNCS, vol. 1114, pp 399\u2013410. Springer (1996)","DOI":"10.1007\/3-540-61532-6_34"},{"key":"9335_CR36","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mun\u0307oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics, no. CP-2003-212448 in NASA Technical Reports, pp 56\u201368 (2003)"},{"key":"9335_CR37","first-page":"5","volume":"1","author":"S Ja\u015bkowski","year":"1934","unstructured":"Ja\u015bkowski, S.: On the rules of suppositions in formal logic. Stud. Logica. 1, 5\u201332 (1934)","journal-title":"Stud. Logica."},{"key":"9335_CR38","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: PRocH: Proof reconstruction for HOL Light. In: Bonacina, M.P. (ed.) CADE-24, LNCS, vol. 7898, pp 267\u2013273. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_18"},{"issue":"2","key":"9335_CR39","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"key":"9335_CR40","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W. (eds.) Complexity of Computer Computations, IBM Research Symposia Series, pp 85\u2013103. Plenum Press (1972)","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"9335_CR41","unstructured":"Klein, G., Nipkow, T., Paulson, L. (eds.): Archive of Formal Proofs. http:\/\/afp.sf.net\/"},{"key":"9335_CR42","unstructured":"Knuth, D.E., Larrabee, T.L., Roberts, P.M.: Mathematical Writing, Mathematical Association of America (1989)"},{"key":"9335_CR43","doi-asserted-by":"crossref","unstructured":"Korovin, K.: Private communication (2013)","DOI":"10.1007\/JHEP08(2013)026"},{"key":"9335_CR44","doi-asserted-by":"crossref","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for Sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013, LNCS, vol. 7998, pp 35\u201350. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_6"},{"key":"9335_CR45","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. North-Holland (1978)"},{"issue":"1","key":"9335_CR46","first-page":"3","volume":"4","author":"R Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications 4(1), 3\u201324 (2005)","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"9335_CR47","doi-asserted-by":"crossref","unstructured":"Meier, A.: TRAMP: transformation of machine-found proofs into natural deduction proofs at the assertion level (system description). In: McAllester, D. (ed.) CADE-17, LNCS, vol. 1831, pp 460\u2013464. Springer (2000)","DOI":"10.1007\/10721959_37"},{"issue":"1","key":"9335_CR48","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35\u201360 (2008)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9335_CR49","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)","journal-title":"J. Appl. Log."},{"key":"9335_CR50","unstructured":"Miller, D., Felty, A.: An integration of resolution and natural deduction theorem proving. In: AAAI-86, vol. I: Science, pp 198\u2013202. Morgan Kaufmann (1986)"},{"key":"9335_CR51","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008, LNCS, vol. 4963, pp 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"9335_CR52","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0167-6423(89)90038-5","volume":"12","author":"T Nipkow","year":"1989","unstructured":"Nipkow, T.: Equational reasoning in Isabelle. Sci. Comput. Program. 12(2), 123\u2013149 (1989)","journal-title":"Sci. Comput. Program."},{"key":"9335_CR53","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics\u2014With Isabelle\/HOL. Springer (2014)","DOI":"10.1007\/978-3-319-10542-0"},{"key":"9335_CR54","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9335_CR55","doi-asserted-by":"crossref","unstructured":"P\u0105k, K.: The methods of improving and reorganizing natural deduction proofs. In: MathUI10 (2010)","DOI":"10.2168\/LMCS-10(3:23)2014"},{"issue":"2","key":"9335_CR56","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/s10817-012-9267-0","volume":"50","author":"K P\u0105k","year":"2013","unstructured":"P\u0105k, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217\u2013228 (2013)","journal-title":"J. Autom. Reason."},{"key":"9335_CR57","doi-asserted-by":"crossref","unstructured":"P\u0105k, K.: Improving legibility of natural deduction proofs is not trivial. Log. Meth. Comput. Sci. 10(3) (2014)","DOI":"10.2168\/LMCS-10(3:23)2014"},{"key":"9335_CR58","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer (1994)","DOI":"10.1007\/BFb0030541"},{"key":"9335_CR59","unstructured":"Paulson, L.C.: Strategic principles in the design of Isabelle. In: CADE-15 Workshop on Strategies in Automated Deduction, pp 11\u201317 (1998)"},{"key":"9335_CR60","first-page":"73","volume":"5","author":"LC Paulson","year":"1999","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with Isabelle. J. Univ. Comp. Sci. 5, 73\u201387 (1999)","journal-title":"J. Univ. Comp. Sci."},{"key":"9335_CR61","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In: Konev, B., Schmidt, R., Schulz, S. (eds.) PAAR-2010, pp 1\u201310 (2010)","DOI":"10.29007\/tnfd"},{"key":"9335_CR62","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010, EPiC, vol. 2, pp 1\u201311. EasyChair (2012)","DOI":"10.29007\/36dt"},{"key":"9335_CR63","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007, LNCS, vol. 4732, pp 232\u2013245. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"9335_CR64","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Analytic and non-analytic proofs. In: Shostak, R.E. (ed.) CADE-7, LNCS, vol. 170, pp 393\u2013413. Springer (1984)","DOI":"10.1007\/978-0-387-34768-4_23"},{"key":"9335_CR65","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C, de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Claessen, K., Kuncak, V. (eds.) FMCAD 2014, pp 195\u2013202. FMCAD Inc. (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"issue":"2\u20133","key":"9335_CR66","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 15(2\u20133), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"1","key":"9335_CR67","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"AJ Robinson","year":"1965","unstructured":"Robinson, A.J.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"issue":"4","key":"9335_CR68","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P Rudnicki","year":"1987","unstructured":"Rudnicki, P.: Obvious inferences. J. Autom. Reason. 3(4), 383\u2013393 (1987)","journal-title":"J. Autom. Reason."},{"key":"9335_CR69","unstructured":"Rudnicki, P., Urban, J.: Escape to ATP for Mizar. In: Fontaine, P., Stump, A. (eds.) PxTP 2011, pp 46\u201359 (2011)"},{"key":"9335_CR70","doi-asserted-by":"crossref","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19, LNCS, vol. 8312, pp 735\u2013743. Springer (2013)","DOI":"10.1007\/978-3-642-45221-5_49"},{"key":"9335_CR71","unstructured":"Smolka, S.J.: Robust, semi-intelligible Isabelle proofs from ATP proofs. B.Sc. thesis, Dept. of Informatics, Technische Universit\u00e4t M\u00fcnchen (2013)"},{"key":"9335_CR72","doi-asserted-by":"crossref","unstructured":"Smolka, S.J., Blanchette, J.C.: Robust, semi-intelligible Isabelle proofs from ATP proofs. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EPiC, vol. 14, pp 117\u2013132. EasyChair (2013)","DOI":"10.29007\/zbdb"},{"key":"9335_CR73","unstructured":"Steckermeier, A.: Extending Isabelle\/HOL with the equality prover Waldmeister. B.Sc. thesis, Dept. of Informatics, Technische Universit\u00e4t M\u00fcnchen (2014)"},{"issue":"1","key":"9335_CR74","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/s10703-012-0163-3","volume":"42","author":"A Stump","year":"2013","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. J. Formal Meth. Sys. Design 42(1), 91\u2013118 (2013)","journal-title":"J. Formal Meth. Sys. Design"},{"key":"9335_CR75","doi-asserted-by":"crossref","unstructured":"Sultana, N., Benzmu\u0307ller, C.: Understanding LEO-II\u2019s proofs. In: Korovin, K., Schulz, S., Ternovska, E. (eds.) IWIL 2012, EPiC, vol. 22, pp 33\u201352. EasyChair (2013)","DOI":"10.29007\/x9c9"},{"key":"9335_CR76","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: System description: SystemOnTPTP. In: McAllester, D. (ed.) CADE-17, LNCS, vol. 1831, pp 406\u2013410. Springer (2000)","DOI":"10.1007\/10721959_31"},{"issue":"4","key":"9335_CR77","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\u2014The FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9335_CR78","doi-asserted-by":"crossref","first-page":"405","DOI":"10.3233\/AIC-140606","volume":"27","author":"G Sutcliffe","year":"2014","unstructured":"Sutcliffe, G.: The CADE-24 automated theorem proving system competition\u2014CASC-24. AI Commun. 27(4), 405\u2013416 (2014)","journal-title":"AI Commun."},{"key":"9335_CR79","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, Frontiers in Artificial Intelligence and Applications, vol. 112, pp 201\u2013215. IOS Press (2004)"},{"key":"9335_CR80","unstructured":"Thiemann, R.: Computing N-th roots using the Babylonian method. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http:\/\/afp.sf.net\/entries\/Sqrt_Babylonian.shtml (2013)"},{"key":"9335_CR81","unstructured":"Urban, J., Sutcliffe, G., Trac, S., Puzis, Y.: Combining Mizar and TPTP semantic presentation and verification tools. In: A. Grabowski, A. Naumowicz (eds.) Computer Reconstruction of the Body of Mathematics, Studies in Logic, Grammar and Rhetoric, vol. 18(31), pp. 121\u2013136. University of Bia\u0142ystok (2009)"},{"key":"9335_CR82","unstructured":"Wampler-Doty, M.: A complete proof of the Robbins conjecture. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs. http:\/\/afp.sf.net\/entries\/Robbins-Conjecture.shtml (2010)"},{"key":"9335_CR83","unstructured":"Weber, T.: Sat-based finite model generation for higher-order logic. Ph.D. thesis, Dept. of Informatics, Technische Universit\u00e4t M\u00fcnchen (2008)"},{"key":"9335_CR84","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22, LNCS, vol. 5663, pp 140\u2013145. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"9335_CR85","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A. (eds.) TPHOLs 1997, LNCS, vol. 1275, pp 307\u2013322. Springer (1997)","DOI":"10.1007\/BFb0028402"},{"key":"9335_CR86","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014A generic framework for human-readable proof documents. In: In: R. Matuszewski, A. Zalewska (eds.) From Insight to Proof\u2014Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, vol. 10(23). University of Bia\u0142ystok (2007)"},{"key":"9335_CR87","doi-asserted-by":"crossref","unstructured":"Wickerson, J., Dodds, M., Parkinson, M.J.: Ribbon proofs for separation logic. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013, LNCS, vol. 7792, pp 189\u2013208. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_12"},{"key":"9335_CR88","unstructured":"Zimmer, J., Meier, A., Sutcliffe, G., Zhan, Y.: Integrated proof transformation services. In: Benzm\u00fcller, C., Windsteiger, W. (eds.) IJCAR WS 7 (2004)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9335-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9335-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9335-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:03:10Z","timestamp":1748491390000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9335-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,12]]},"references-count":88,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,2]]}},"alternative-id":["9335"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9335-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7,12]]}}}