{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T13:25:19Z","timestamp":1778678719874,"version":"3.51.4"},"reference-count":75,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,1,20]],"date-time":"2018-01-20T00:00:00Z","timestamp":1516406400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-017-9447-z","type":"journal-article","created":{"date-parts":[[2018,1,20]],"date-time":"2018-01-20T01:49:20Z","timestamp":1516412960000},"page":"455-484","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Formalization of the Resolution Calculus for First-Order Logic"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9212-6150","authenticated-orcid":false,"given":"Anders","family":"Schlichtkrull","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,1,20]]},"reference":[{"issue":"3","key":"9447_CR1","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1145\/321592.321603","volume":"17","author":"R Anderson","year":"1970","unstructured":"Anderson, R., Bledsoe, W.W.: A linear format for resolution with merging and a new technique for establishing completeness. J. ACM 17(3), 525\u2013534 (1970)","journal-title":"J. ACM"},{"key":"9447_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"9447_CR3","unstructured":"Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of Knuth\u2013Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Lambda_Free_KBOs.shtml , Formal proof development"},{"key":"9447_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-4129-7","volume-title":"Mathematical Logic for Computer Science","author":"M Ben-Ari","year":"2012","unstructured":"Ben-Ari, M.: Mathematical Logic for Computer Science, 3rd edn. Springer, New York (2012)","edition":"3"},{"key":"9447_CR5","unstructured":"Berghofer, S.: First-order logic according to Fitting. Archive of Formal Proofs (2007). http:\/\/isa-afp.org\/entries\/FOL-Fitting.shtml , Formal proof development"},{"issue":"1","key":"9447_CR6","doi-asserted-by":"publisher","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":"9447_CR7","first-page":"25","volume-title":"IJCAR 2016, LNCS","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 25\u201344. Springer, New York (2016)"},{"key":"9447_CR8","first-page":"93","volume-title":"ITP 2014, LNCS","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014, LNCS, vol. 8558, pp. 93\u2013110. Springer, New York (2014)"},{"key":"9447_CR9","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Abstract completeness. Archive of Formal Proofs (2014). http:\/\/isa-afp.org\/entries\/Abstract_Completeness.shtml , Formal proof development"},{"key":"9447_CR10","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion: a proof assistant perspective. In:\u00a0Fisher, K.,\u00a0Reppy, J. (eds.) ICFP\u201915, pp. 192\u2013204. ACM (2015)","DOI":"10.1145\/2784731.2784732"},{"key":"9447_CR11","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Abstract soundness. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Abstract_Soundness.shtml , Formal proof development"},{"issue":"1","key":"9447_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10817-016-9391-3","volume":"58","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149\u2013179 (2017)","journal-title":"J. Autom. Reason."},{"key":"9447_CR13","unstructured":"Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of recursive path orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Lambda_Free_RPOs.shtml , Formal proof development"},{"issue":"1","key":"9447_CR14","first-page":"49","volume":"13","author":"P Braselmann","year":"2005","unstructured":"Braselmann, P., Koepke, P.: G\u00f6del completeness theorem. Formaliz. Math. 13(1), 49\u201353 (2005)","journal-title":"Formaliz. Math."},{"issue":"1","key":"9447_CR15","first-page":"33","volume":"13","author":"P Braselmann","year":"2005","unstructured":"Braselmann, P., Koepke, P.: A sequent calculus for first-order logic. Formaliz. Math. 13(1), 33\u201339 (2005)","journal-title":"Formaliz. Math."},{"key":"9447_CR16","first-page":"123","volume-title":"ITP 2016, LNCS","author":"J Breitner","year":"2016","unstructured":"Breitner, J.: Visual theorem proving with the Incredible Proof Machine. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, LNCS, vol. 9807, pp. 123\u2013139. Springer, New York (2016)"},{"key":"9447_CR17","unstructured":"Breitner, J., Lohner, D.: The meta theory of the Incredible Proof Machine. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Incredible_Proof_Machine.shtml , Formal proof development"},{"key":"9447_CR18","first-page":"111","volume-title":"CADE-9, LNCS","author":"A Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE-9, LNCS, vol. 310, pp. 111\u2013120. Springer, New York (1988)"},{"key":"9447_CR19","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"CL Chang","year":"1973","unstructured":"Chang, C.L., Lee, R.C.T.: Symbolic Logic and Mechanical Theorem Proving, 1st edn. Academic Press, Cambridge (1973)","edition":"1"},{"key":"9447_CR20","unstructured":"Coen, M., Slind, K., Krauss, A.: Theory unification. Isabelle. http:\/\/isabelle.in.tum.de\/library\/HOL\/HOL-ex\/Unification.html . Accessed 13 Dec 2017"},{"key":"9447_CR21","unstructured":"Coen, M.D.: Interactive program derivation. Ph.D. thesis, University of Cambridge (1992). http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-272.html"},{"key":"9447_CR22","unstructured":"Corbin, J., Bidoit, M.: A rehabilitation of Robinson\u2019s unification algorithm. In: IFIP Congress, pp. 909\u2013914 (1983)"},{"key":"9447_CR23","doi-asserted-by":"crossref","unstructured":"Davis, J., Myreen, M.O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it). J. Autom. Reason. (2015)","DOI":"10.1007\/s10817-015-9324-6"},{"key":"9447_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2355-7","volume-title":"Mathematical Logic","author":"H Ebbinghaus","year":"1994","unstructured":"Ebbinghaus, H., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Springer, New York (1994)","edition":"2"},{"key":"9447_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1996). Second Edition","edition":"2"},{"key":"9447_CR26","unstructured":"Gebhard, H.: Beweisplanung f\u00fcr die Beweise der Vollst\u00e4ndigkeit verschiedener Resolutionskalk\u00fcle in $$\\rm \\Omega \\it $$ \u03a9 MEGA. Master\u2019s thesis, Saarland University (1999)"},{"key":"9447_CR27","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-37651-1_5","volume-title":"Programming Logics: Essays in Memory of Harald Ganzinger, LNCS","author":"J Goubault-Larrecq","year":"2013","unstructured":"Goubault-Larrecq, J., Jouannaud, J.P.: The blossom of finite semantic trees. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics: Essays in Memory of Harald Ganzinger, LNCS, pp. 90\u2013122. Springer, New York (2013)"},{"key":"9447_CR28","first-page":"153","volume-title":"TPHOL\u2019s 1998, LNCS","author":"J Harrison","year":"1998","unstructured":"Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOL\u2019s 1998, LNCS, vol. 1497, pp. 153\u2013170. Springer, New York (1998)"},{"key":"9447_CR29","first-page":"177","volume-title":"IJCAR 2006, LNCS","author":"J Harrison","year":"2006","unstructured":"Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006, LNCS, vol. 4130, pp. 177\u2013191. Springer, New York (2006)"},{"key":"9447_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)"},{"key":"9447_CR31","unstructured":"Ilik, D.: Constructive completeness proofs and delimited control. Ph.D. thesis, \u00c9cole Polytechnique (2010). https:\/\/tel.archives-ouvertes.fr\/tel-00529021\/document"},{"issue":"11","key":"9447_CR32","doi-asserted-by":"publisher","first-page":"1367","DOI":"10.1016\/j.apal.2010.04.007","volume":"161","author":"D Ilik","year":"2010","unstructured":"Ilik, D., Lee, G., Herbelin, H.: Kripke models for classical logic. Ann. Pure Appl. Log. 161(11), 1367\u20131378 (2010)","journal-title":"Ann. Pure Appl. Log."},{"key":"9447_CR33","unstructured":"IsaFoL authors: IsaFoL: Isabelle Formalization of Logic. https:\/\/bitbucket.org\/isafol\/isafol . Accessed 13 Dec 2017"},{"key":"9447_CR34","unstructured":"IsaFoR developers: An Isabelle\/HOL formalization of rewriting for certified termination analysis. http:\/\/cl-informatik.uibk.ac.at\/software\/ceta\/ . Accessed 13 Dec 2017"},{"key":"9447_CR35","unstructured":"Jensen, A.B., Schlichtkrull, A., Villadsen, J.: Verification of an LCF-style first-order prover with equality. In: Isabelle Workshop 2016 Associated with ITP 2016 (2016)"},{"key":"9447_CR36","unstructured":"Jensen, A.B., Schlichtkrull, A., Villadsen, J.: First-order logic according to Harrison. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/FOL_Harrison.shtml , Formal proof development"},{"key":"9447_CR37","unstructured":"Kohlhase, M.: Theorem prover museum \u2013 OMEGA theories \u2013 folders: propositional-logic, resolution, proof-theory, prop-res. https:\/\/github.com\/theoremprover-museum\/OMEGA\/tree\/master\/theories . Accessed 13 Dec 2017"},{"issue":"4","key":"9447_CR38","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A Krauss","year":"2010","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303\u2013336 (2010)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9447_CR39","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-015-9357-x","volume":"56","author":"R Kumar","year":"2016","unstructured":"Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: Self-formalisation of higher-order logic: semantics, soundness, and a verified implementation. J. Autom. Reason. 56(3), 221\u2013259 (2016)","journal-title":"J. Autom. Reason."},{"key":"9447_CR40","first-page":"237","volume-title":"CADE-26, LNCS","author":"P Lammich","year":"2017","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de Moura, L. (ed.) CADE-26, LNCS, vol. 10395, pp. 237\u2013254. Springer, New York (2017)"},{"key":"9447_CR41","first-page":"457","volume-title":"SAT 2017, LNCS","author":"P Lammich","year":"2017","unstructured":"Lammich, P.: The GRAT tool chain. In: Gaspers, S., Walsh, T. (eds.) SAT 2017, LNCS, vol. 10491, pp. 457\u2013463. Springer, New York (2017)"},{"issue":"1","key":"9447_CR42","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1002\/malq.19890350109","volume":"35","author":"A Leitsch","year":"1989","unstructured":"Leitsch, A.: On different concepts of resolution. Math. Log. Q. 35(1), 71\u201377 (1989)","journal-title":"Math. Log. Q."},{"key":"9447_CR43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-60605-2","volume-title":"The Resolution Calculus","author":"A Leitsch","year":"1997","unstructured":"Leitsch, A.: The Resolution Calculus. Springer, New York (1997)"},{"issue":"1","key":"9447_CR44","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/0167-6423(81)90004-6","volume":"1","author":"Z Manna","year":"1981","unstructured":"Manna, Z., Waldinger, R.: Deductive synthesis of the unification algorithm. Sci. Comput. Program. 1(1), 5\u201348 (1981)","journal-title":"Sci. Comput. Program."},{"key":"9447_CR45","unstructured":"Margetson, J., Ridge, T.: Completeness theorem. Archive of Formal Proofs (2004). http:\/\/isa-afp.org\/entries\/Completeness.shtml , Formal proof development"},{"key":"9447_CR46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, New York (2014)"},{"key":"9447_CR47","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Springer, New York (2002)"},{"issue":"2","key":"9447_CR48","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0167-6423(85)90009-7","volume":"5","author":"LC Paulson","year":"1985","unstructured":"Paulson, L.C.: Verifying the unification algorithm in LCF. Sci. Comput. Program. 5(2), 143\u2013169 (1985)","journal-title":"Sci. Comput. Program."},{"key":"9447_CR49","unstructured":"Paulson, L.C.: G\u00f6del\u2019s incompleteness theorems. Archive of Formal Proofs (2013). http:\/\/isa-afp.org\/entries\/Incompleteness.shtml , Formal proof development"},{"issue":"03","key":"9447_CR50","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1017\/S1755020314000112","volume":"7","author":"LC Paulson","year":"2014","unstructured":"Paulson, L.C.: A machine-assisted proof of G\u00f6del\u2019s incompleteness theorems for the theory of hereditarily finite sets. Rev. Symb. Log. 7(03), 484\u2013498 (2014)","journal-title":"Rev. Symb. Log."},{"issue":"1","key":"9447_CR51","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-015-9322-8","volume":"55","author":"LC Paulson","year":"2015","unstructured":"Paulson, L.C.: A mechanised proof of G\u00f6del\u2019s incompleteness theorems using Nominal Isabelle. J. Autom. Reason. 55(1), 1\u201337 (2015)","journal-title":"J. Autom. Reason."},{"key":"9447_CR52","unstructured":"Peltier, N.: Propositional resolution and prime implicates generation. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/PropResPI.shtml , Formal proof development"},{"key":"9447_CR53","unstructured":"Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/SuperCalc.shtml , Formal proof development"},{"key":"9447_CR54","unstructured":"Persson, H.: Constructive completeness of intuitionistic predicate logic. Ph.D. thesis, Chalmers University of Technology (1996). http:\/\/web.archive.org\/web\/19970715002824\/http:\/\/www.cs.chalmers.se\/~henrikp\/Lic\/"},{"key":"9447_CR55","doi-asserted-by":"crossref","unstructured":"Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning, vol.\u00a02, pp. 1853\u20131964 (2001)","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"9447_CR56","unstructured":"Raffalli, C.: Krivine\u2019s abstract completeness proof for classical predicate logic. https:\/\/github.com\/craff\/phox\/blob\/master\/examples\/complete.phx (2005, possibly earlier). Accessed 13 Dec 2017"},{"key":"9447_CR57","first-page":"292","volume-title":"CADE-16, LNCS","author":"A Riazanov","year":"1999","unstructured":"Riazanov, A., Voronkov, A.: Vampire. In: Ganzinger, H. (ed.) CADE-16, LNCS, vol. 1632, pp. 292\u2013296. Springer, New York (1999)"},{"key":"9447_CR58","unstructured":"Ridge, T.: A mechanically verified, efficient, sound and complete theorem prover for first order logic. Archive of Formal Proofs (2004). http:\/\/isa-afp.org\/entries\/Verified-Prover.shtml , Formal proof development"},{"key":"9447_CR59","first-page":"294","volume-title":"TPHOL\u2019s 2005, LNCS","author":"T Ridge","year":"2005","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOL\u2019s 2005, LNCS, vol. 3603, pp. 294\u2013309. Springer, New York (2005)"},{"issue":"1","key":"9447_CR60","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"9447_CR61","first-page":"77","volume":"3","author":"JA Robinson","year":"1968","unstructured":"Robinson, J.A.: The generalized resolution principle. Mach. Intell. 3, 77\u201393 (1968)","journal-title":"Mach. Intell."},{"issue":"1","key":"9447_CR62","first-page":"67","volume":"37","author":"JL Ruiz-Reina","year":"2006","unstructured":"Ruiz-Reina, J.L., Mart\u00edn-Mateos, F.J., Alonso, J.A., Hidalgo, M.J.: Formal correctness of a quadratic unification algorithm. J. Autom. Reason. 37(1), 67\u201392 (2006)","journal-title":"J. Autom. Reason."},{"key":"9447_CR63","unstructured":"Schlichtkrull, A.: Formalization of resolution calculus in Isabelle. Master\u2019s thesis, Technical University of Denmark (2015). https:\/\/people.compute.dtu.dk\/andschl\/Thesis.pdf"},{"key":"9447_CR64","first-page":"341","volume-title":"ITP 2016, LNCS","author":"A Schlichtkrull","year":"2016","unstructured":"Schlichtkrull, A.: Formalization of the resolution calculus for first-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016, LNCS, vol. 9807, pp. 341\u2013357. Springer, New York (2016)"},{"key":"9447_CR65","unstructured":"Schlichtkrull, A.: The resolution calculus for first-order logic. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Resolution_FOL.shtml , Formal proof development"},{"key":"9447_CR66","doi-asserted-by":"crossref","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalization of Bachmair and Ganzinger\u2019s simple ordered resolution prover. https:\/\/bitbucket.org\/isafol\/isafol\/src\/master\/Ordered_Resolution_Prover\/ . Accessed 13 Dec 2017","DOI":"10.29007\/pn71"},{"key":"9447_CR67","unstructured":"Schlichtkrull, A., Villadsen, J.: Paraconsistency. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Paraconsistency.shtml , Formal proof development"},{"issue":"3","key":"9447_CR68","doi-asserted-by":"crossref","first-page":"199","DOI":"10.2478\/v10037-012-0023-z","volume":"20","author":"JJ Schl\u00f6der","year":"2012","unstructured":"Schl\u00f6der, J.J., Koepke, P.: The G\u00f6del completeness theorem for uncountable languages. Formaliz. Math. 20(3), 199\u2013203 (2012)","journal-title":"Formaliz. Math."},{"key":"9447_CR69","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, New York (2013)","DOI":"10.1007\/978-3-642-45221-5_49"},{"key":"9447_CR70","unstructured":"Shankar, N.: Proof-checking metamathematics. Ph.D. thesis, University of Texas (1986)"},{"key":"9447_CR71","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569883","volume-title":"Metamathematics, Machines, and G\u00f6del\u2019s Proof","author":"N Shankar","year":"1994","unstructured":"Shankar, N.: Metamathematics, Machines, and G\u00f6del\u2019s Proof. Cambridge University Press, Cambridge (1994)"},{"key":"9447_CR72","unstructured":"Slind, K.: Reasoning about terminating functional programs. Ph.D. thesis, Technical University of Munich (1999). https:\/\/mediatum.ub.tum.de\/?id=601660"},{"key":"9447_CR73","unstructured":"Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: F.\u00a0van Raamsdonk (ed.) RTA \u201913, LIPIcs, vol.\u00a021, pp. 287\u2013302. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2013)"},{"key":"9447_CR74","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, New York (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"9447_CR75","first-page":"167","volume-title":"TPHOL\u2019s 1999, LNCS","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOL\u2019s 1999, LNCS, vol. 1690, pp. 167\u2013183. Springer, New York (1999)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9447-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9447-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9447-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,9]],"date-time":"2019-10-09T12:22:10Z","timestamp":1570623730000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9447-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,20]]},"references-count":75,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9447"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9447-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,20]]},"assertion":[{"value":"30 March 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 December 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 January 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}