{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:36:08Z","timestamp":1761510968692,"version":"3.41.2"},"reference-count":53,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,28]],"date-time":"2012-03-28T00:00:00Z","timestamp":1332892800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We propose a synthesis of the two proof styles of interactive theorem\nproving: the procedural style (where proofs are scripts of commands, like in\nCoq) and the declarative style (where proofs are texts in a controlled natural\nlanguage, like in Isabelle\/Isar). Our approach combines the advantages of the\ndeclarative style - the possibility to write formal proofs like normal\nmathematical text - and the procedural style - strong automation and help with\nshaping the proofs, including determining the statements of intermediate steps.\nOur approach is new, and differs significantly from the ways in which the\nprocedural and declarative proof styles have been combined before in the\nIsabelle, Ssreflect and Matita systems. Our approach is generic and can be\nimplemented on top of any procedural interactive theorem prover, regardless of\nits architecture and logical foundations. To show the viability of our proposed\napproach, we fully implemented it as a proof interface called miz3, on top of\nthe HOL Light interactive theorem prover. The declarative language that this\ninterface uses is a slight variant of the language of the Mizar system, and can\nbe used for any interactive theorem prover regardless of its logical\nfoundations. The miz3 interface allows easy access to the full set of tactics\nand formal libraries of HOL Light, and as such has \"industrial strength\". Our\napproach gives a way to automatically convert any procedural proof to a\ndeclarative counterpart, where the converted proof is similar in size to the\noriginal. As all declarative systems have essentially the same proof language,\nthis gives a straightforward way to port proofs between interactive theorem\nprovers.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:30)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":13,"title":["A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Freek","family":"Wiedijk","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,28]]},"reference":[{"key":"10.2168\/LMCS-8(1:30)2012_abr:96","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"10.2168\/LMCS-8(1:30)2012_agd:xx","unstructured":"Agda Development Team. The Agda Wiki. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php."},{"key":"10.2168\/LMCS-8(1:30)2012_asp:coe:tas:zac:07","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_2"},{"issue":"1-3","key":"10.2168\/LMCS-8(1:30)2012_asp:03","first-page":"27","volume":"38","author":"Andrea Asperti et al","year":"2003","journal-title":"Annals of Mathematics and Artificial Intelligence 38(1-3):27-46, 2003"},{"key":"10.2168\/LMCS-8(1:30)2012_asp:weg:02","unstructured":"Andrea Asperti and Bernd Wegner. MOWGLI - A New Approach for the Content Description in Digital Documents. InProc. of the 9th Intl. Conference on Electronic Resources and the Social Role of Libraries in the Future, volume 1, Autonomous Republic of Crimea, Ukraine, 2002."},{"key":"10.2168\/LMCS-8(1:30)2012_asp:00","doi-asserted-by":"crossref","unstructured":"David Aspinall. Proof General: A generic tool for proof development. InEuropean Joint Conferences on Theory and Practice of Software (ETAPS), 2000.","DOI":"10.1007\/3-540-46419-0_3"},{"key":"10.2168\/LMCS-8(1:30)2012_bar:03","doi-asserted-by":"crossref","unstructured":"Henk Barendregt. Towards an Interactive Mathematical Proof Language. In F. Kamareddine, editor,Thirty Five Years of Automath, pages 25-36. Kluwer, 2003.","DOI":"10.1007\/978-94-017-0253-9_2"},{"issue":"1835","key":"10.2168\/LMCS-8(1:30)2012_bar:wie:06","first-page":"2351","volume":"363","author":"Henk Barendregt and Freek Wiedijk","year":"2006","journal-title":"Transactions A of the Royal Society 2006"},{"key":"10.2168\/LMCS-8(1:30)2012_bea:98","unstructured":"Douglas Beaver et al. Amazon.com Interview: Larry Wall. The father of Perl talks about XML, Unicode, the Win32 port, and the philosophy behind the language, http:\/\/www.amazon.com\/gp\/feature.html?docId=7137, 1998."},{"key":"10.2168\/LMCS-8(1:30)2012_buc:jeb:kri:mar:vas:97","doi-asserted-by":"crossref","unstructured":"B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, and D. Vasaru. An Overview on the Theorema project. In W. Kuechlin, editor,Proceedings of ISSAC'97 (International Symposium on Symbolic and Algebraic Computation), Maui, Hawaii, 1997. ACM Press.","DOI":"10.1145\/258726.258853"},{"key":"10.2168\/LMCS-8(1:30)2012_cai:gow:04","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.entcs.2003.12.028","volume":"93","author":"Paul Cairns and Jeremy Gow","year":"2004","journal-title":"Electronic Notes in Theoretical Computer Science 2004"},{"key":"10.2168\/LMCS-8(1:30)2012_con:all:bro:cle:cre:har:how:kno:men:pan:sas:smi:86","unstructured":"Robert L. Constable, Stuart F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, Douglas J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith.Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ, 1986."},{"key":"10.2168\/LMCS-8(1:30)2012_coq:10","unstructured":"Coq Development Team.The Coq Proof Assistant Reference Manual, 2010. Pierre Corbineau. A declarative proof language for the Coq proof assistant. InTYPES 2007 : Types for Proofs and Programs, number 4941 in LNCS. Springer-Verlag, 2007."},{"key":"10.2168\/LMCS-8(1:30)2012_bru:87","unstructured":"N.G. de Bruijn. The Mathematical Vernacular, a language for mathematics with typed sets. In P. Dybjer et al., editors,Proceedings of the Workshop on Programming Languages, Marstrand, Sweden, 1987."},{"key":"10.2168\/LMCS-8(1:30)2012_fox:03","unstructured":"Anthony Fox. Formal Specification and Verification of ARM6. In D.A. Basin and B. Wolff, editors,TPHOLs 2003, volume 2758 ofLNCS. Springer, 2003."},{"key":"10.2168\/LMCS-8(1:30)2012_gon:06","unstructured":"Georges Gonthier. A computer-checked proof of the Four Colour Theorem. http:\/\/research.microsoft.com\/ gonthier\/4colproof.pdf, 2006."},{"key":"10.2168\/LMCS-8(1:30)2012_gon:mah:tas:08","unstructured":"Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA, 2008."},{"key":"10.2168\/LMCS-8(1:30)2012_gor:mel:93","unstructured":"Mike Gordon and Tom Melham, editors.Introduction to HOL. Cambridge University Press, Cambridge, 1993."},{"key":"10.2168\/LMCS-8(1:30)2012_gra:kor:nau:10","first-page":"153","volume":"3","author":"Adam Grabowski, Artur Kornilowicz,","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"10.2168\/LMCS-8(1:30)2012_gui:03","unstructured":"Fr\u00e9d\u00e9rique Guilhot. Proof explanations: using natural language and graph view, 2003. presentation for the MoWGLI project."},{"key":"10.2168\/LMCS-8(1:30)2012_hal:11","unstructured":"Tom Hales. Mathematics in the Age of the Turing Machine, 2011. To appear in 2012 in a special volume of Lecture Notes in Logic (CUP) in commemoration of the centennial of Turing's birth."},{"key":"10.2168\/LMCS-8(1:30)2012_har:xx","unstructured":"John Harrison. The HOL Light theorem prover. http:\/\/www.cl.cam.ac.uk\/ jrh13\/hol-light\/."},{"key":"10.2168\/LMCS-8(1:30)2012_har:96","doi-asserted-by":"crossref","unstructured":"John Harrison. A Mizar Mode for HOL. In J. von Wright, J. Grundy, and J. Harrison, editors,TPHOLs '96, volume 1125 ofLNCS, 1996.","DOI":"10.1007\/BFb0105406"},{"key":"10.2168\/LMCS-8(1:30)2012_har:96:1","doi-asserted-by":"crossref","unstructured":"John Harrison. Optimizing Proof Search in Model Elimination. In M. A. McRobbie and J. K. Slaney, editors,13th International Conference on Automated Deduction, volume 1104 ofLNCS, pages 313-327, New Brunswick, NJ, 1996. Springer-Verlag.","DOI":"10.1007\/3-540-61511-3_97"},{"key":"10.2168\/LMCS-8(1:30)2012_har:96:2","doi-asserted-by":"crossref","unstructured":"John Harrison. Proof Style. In Eduardo Gim\u00e9nez and Christine Paulin-M\u00f6hring, editors,Types for Proofs and Programs: International Workshop TYPES'96, volume 1512 ofLNCS, pages 154-172, Aussois, France, 1996. Springer-Verlag.","DOI":"10.1007\/BFb0097791"},{"key":"10.2168\/LMCS-8(1:30)2012_har:00","unstructured":"John Harrison.The HOL Light manual (1.1), 2000. John Harrison.HOL Light Tutorial (for version 2.20), 2007."},{"key":"10.2168\/LMCS-8(1:30)2012_har:08","doi-asserted-by":"crossref","unstructured":"John Harrison. Formalizing an Analytic Proof of the Prime Number Theorem. In R. Boulton, J. Hurd, and K. Slind, editors,Tools and Techniques for Verification of System Infrastructure, pages 243-261. The Royal Society, 2008.","DOI":"10.1007\/s10817-009-9145-6"},{"key":"10.2168\/LMCS-8(1:30)2012_hut:rya:04","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275"},{"key":"10.2168\/LMCS-8(1:30)2012_kal:wie:09","doi-asserted-by":"crossref","unstructured":"Cezary Kaliszyk and Freek Wiedijk. Merging procedural and declarative proof. In S. Berardi, F. Damiani, and U. De'Liquoro, editors,TYPES 2008, 2009.","DOI":"10.1007\/978-3-642-02444-3_13"},{"key":"10.2168\/LMCS-8(1:30)2012_kau:man:moo:00","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"10.2168\/LMCS-8(1:30)2012_kle:09","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"10.2168\/LMCS-8(1:30)2012_ler:06","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. Formal Certification of a Compiler Back-end, or: Programming a Compiler with a Proof Assistant. InPOPL'06, 2006.","DOI":"10.1145\/1111037.1111042"},{"key":"10.2168\/LMCS-8(1:30)2012_lem:00","unstructured":"Lemma 1 Ltd.ProofPower - Description. Lemma 1 Ltd., 2000."},{"key":"10.2168\/LMCS-8(1:30)2012_mcb:mck:04","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"10.2168\/LMCS-8(1:30)2012_meg:97","unstructured":"Norman D. Megill. Metamath, A Computer Language for Pure Mathematics. http:\/\/us.metamath.org\/downloads\/metamath.pdf, 1997."},{"key":"10.2168\/LMCS-8(1:30)2012_nip:pau:wen:02","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow, Larry Paulson, and Markus Wenzel.Isabelle\/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 ofLNCS. Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"10.2168\/LMCS-8(1:30)2012_owr:rus:sha:92","doi-asserted-by":"crossref","unstructured":"Sam Owre, John M. Rushby, and Natarajan Shankar. PVS: A Prototype Verification System. In D. Kapur, editor,11th International Conference on Automated Deduction (CADE), volume 607 ofLNAI, pages 748-752, Berlin, Heidelberg, New York, 1992. Springer.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"10.2168\/LMCS-8(1:30)2012_pas:07","unstructured":"Andrei Paskevich. The syntax and semantics of the ForTheL language. http:\/\/nevidal.org\/download\/forthel.pdf."},{"key":"10.2168\/LMCS-8(1:30)2012_pel:00","unstructured":"Jeff Pelletier. A History of Natural Deduction and Elementary Logic Textbooks. In J. Woods and B. Brown, editors,Logical Consequence: Rival Approaches and New Studies, Vol. 1. Hermes Science Pubs., 2000."},{"key":"10.2168\/LMCS-8(1:30)2012_pfe:sch:02","unstructured":"Frank Pfenning and Carsten Schuermann.Twelf User's Guide, Version 1.4, 2002. http:\/\/www-2.cs.cmu.edu\/ twelf\/guide-1-4\/twelf.ps."},{"key":"10.2168\/LMCS-8(1:30)2012_pol:98","doi-asserted-by":"crossref","unstructured":"Randy Pollack. How to Believe a Machine-Checked Proof. In G. Sambin and J. Smith, editors,Twenty-Five Years of Constructive Type Theory. Oxford University Press, Oxford, 1998.","DOI":"10.7146\/brics.v4i18.18945"},{"key":"10.2168\/LMCS-8(1:30)2012_pho:xx","unstructured":"Christophe Raffalli. The PhoX Proof Assistant. http:\/\/www.lama.univ-savoie.fr\/ RAFFALLI\/phox.html."},{"key":"10.2168\/LMCS-8(1:30)2012_coe:10","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s10817-009-9136-7","volume":"44","author":"Claudio Sacerdoti Coen","year":"2010","journal-title":"J. Autom. Reason."},{"key":"10.2168\/LMCS-8(1:30)2012_smu:90","unstructured":"Raymond Smullyan.What Is the Name of this Book?Penguin Books Ltd, 1990."},{"issue":"4","key":"10.2168\/LMCS-8(1:30)2012_urb:06:1","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1016\/j.jal.2005.10.004","volume":"4","author":"Josef Urban","year":"2006","journal-title":"J. Applied Logic"},{"key":"10.2168\/LMCS-8(1:30)2012_wae:71","doi-asserted-by":"crossref","unstructured":"B.L. van der Waerden.Algebra I. Springer-Verlag, 1971. Achte Auflage.","DOI":"10.1007\/978-3-642-96044-4"},{"key":"10.2168\/LMCS-8(1:30)2012_wen:02","unstructured":"Markus Wenzel.Isabelle\/Isar -- a versatile environment for human-readable formal proof documents. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 2002. http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html."},{"key":"10.2168\/LMCS-8(1:30)2012_wen:02:1","unstructured":"Markus Wenzel.The Isabelle\/Isar Reference Manual. TU M\u00fcnchen, 2002."},{"key":"10.2168\/LMCS-8(1:30)2012_wen:wie:02","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1023\/A:1021935419355","volume":"29","author":"Markus Wenzel and Freek Wiedijk","year":"2002","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(1:30)2012_wie:01","doi-asserted-by":"crossref","unstructured":"Freek Wiedijk. Mizar Light for {HOL Light}. In R. J. Boulton and P. B. Jackson, editors,TPHOLs 2001, volume 2152 ofLNCS, 2001.","DOI":"10.1007\/3-540-44755-5_26"},{"key":"10.2168\/LMCS-8(1:30)2012_wie:04","doi-asserted-by":"crossref","unstructured":"Freek Wiedijk. Formal Proof Sketches. In S. Berardi, M. Coppo, and F. Damiani, editors,TYPES 2003, volume 3085 ofLNCS, pages 378-393, 2004.","DOI":"10.1007\/978-3-540-24849-1_24"},{"key":"10.2168\/LMCS-8(1:30)2012_wie:06","doi-asserted-by":"crossref","unstructured":"Freek Wiedijk, editor.The Seventeen Provers of the World, volume 3600 ofLNCS. Springer, 2006. With a foreword by Dana S. Scott.","DOI":"10.1007\/11542384"},{"key":"10.2168\/LMCS-8(1:30)2012_wie:07:2","doi-asserted-by":"crossref","unstructured":"Freek Wiedijk. Mizar's Soft Type System. In K. Schneider and J. Brandt, editors,Theorem Proving in Higher Order Logics 2007, volume 4732 ofLNCS, pages 383-399, 2007.","DOI":"10.1007\/978-3-540-74591-4_28"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1046\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1046\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:03Z","timestamp":1681243323000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1046"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,28]]},"references-count":53,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:30)2012","relation":{"references":[{"id-type":"doi","id":"10.1007\/978-3-642-96044-4","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1201.3601","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1201.3601","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,3,28]]},"article-number":"1046"}}