{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T04:36:30Z","timestamp":1741667790388,"version":"3.38.0"},"reference-count":32,"publisher":"SAGE Publications","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2018,5,17]]},"DOI":"10.3233\/aic-180764","type":"journal-article","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T15:19:03Z","timestamp":1523632743000},"page":"281-299","source":"Crossref","is-referenced-by-count":10,"title":["Programming and verifying a declarative first-order prover in Isabelle\/HOL"],"prefix":"10.1177","volume":"31","author":[{"given":"Alexander Birch","family":"Jensen","sequence":"first","affiliation":[{"name":"DTU Compute, Technical University of Denmark, 2800 Kongens Lyngby, Denmark. E-mails:\u00a0aleje@dtu.dk,\u00a0jobla@dtu.dk,\u00a0andschl@dtu.dk,\u00a0jovi@dtu.dk"}]},{"given":"John Bruntse","family":"Larsen","sequence":"additional","affiliation":[{"name":"DTU Compute, Technical University of Denmark, 2800 Kongens Lyngby, Denmark. E-mails:\u00a0aleje@dtu.dk,\u00a0jobla@dtu.dk,\u00a0andschl@dtu.dk,\u00a0jovi@dtu.dk"}]},{"given":"Anders","family":"Schlichtkrull","sequence":"additional","affiliation":[{"name":"DTU Compute, Technical University of Denmark, 2800 Kongens Lyngby, Denmark. E-mails:\u00a0aleje@dtu.dk,\u00a0jobla@dtu.dk,\u00a0andschl@dtu.dk,\u00a0jovi@dtu.dk"}]},{"given":"J\u00f8rgen","family":"Villadsen","sequence":"additional","affiliation":[{"name":"DTU Compute, Technical University of Denmark, 2800 Kongens Lyngby, Denmark. E-mails:\u00a0aleje@dtu.dk,\u00a0jobla@dtu.dk,\u00a0andschl@dtu.dk,\u00a0jovi@dtu.dk"}]}],"member":"179","reference":[{"key":"10.3233\/AIC-180764_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_11"},{"issue":"1","key":"10.3233\/AIC-180764_ref3","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10817-016-9391-3","article-title":"Soundness and completeness proofs by coinductive methods","volume":"58","author":"Blanchette","year":"2017","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"10.3233\/AIC-180764_ref4","first-page":"33","article-title":"A sequent calculus for first-order logic","volume":"13","author":"Braselmann","year":"2005","journal-title":"Formalized Mathematics"},{"issue":"1","key":"10.3233\/AIC-180764_ref5","first-page":"49","article-title":"G\u00f6del completeness theorem","volume":"13","author":"Braselmann","year":"2005","journal-title":"Formalized Mathematics"},{"key":"10.3233\/AIC-180764_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_8"},{"key":"10.3233\/AIC-180764_ref7","unstructured":"A.\u00a0Church, Introduction to Mathematical Logic, Princeton University Press, Princeton, 1956."},{"issue":"1","key":"10.3233\/AIC-180764_ref8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s12046-009-0001-5","article-title":"Proof assistants: History, ideas and future","volume":"34","author":"Geuvers","year":"2009","journal-title":"Sadhana"},{"key":"10.3233\/AIC-180764_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"10.3233\/AIC-180764_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"10.3233\/AIC-180764_ref11","doi-asserted-by":"crossref","unstructured":"R.\u00a0H\u00e4hnle, Tableaux and related methods, in: Handbook of Automated Reasoning, Vol. 1, 2001, pp.\u00a0101\u2013178.","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"key":"10.3233\/AIC-180764_ref12","doi-asserted-by":"crossref","unstructured":"J.\u00a0Harrison, Towards self-verification of HOL Light, in: IJCAR 2006, U.\u00a0Furbach and N.\u00a0Shankar, eds, LNCS, Vol.\u00a04130, Springer, 2006, pp.\u00a0177\u2013191.","DOI":"10.1007\/11814771_17"},{"key":"10.3233\/AIC-180764_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430"},{"key":"10.3233\/AIC-180764_ref14","unstructured":"J.\u00a0Harrison, J.\u00a0Urban and F.\u00a0Wiedijk, History of interactive theorem proving, in: Handbook of the History of Logic, Vol.\u00a09: Computational Logic, J.\u00a0Siekmann, ed., Elsevier, 2014, pp.\u00a0135\u2013214."},{"key":"10.3233\/AIC-180764_ref17","unstructured":"A.B.\u00a0Jensen, A.\u00a0Schlichtkrull and J.\u00a0Villadsen, Verification of an LCF-style first-order prover with equality, in: Isabelle Workshop, 2016."},{"issue":"3","key":"10.3233\/AIC-180764_ref20","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-015-9357-x","article-title":"Self-formalisation of higher-order logic: Semantics, soundness, and a verified implementation","volume":"56","author":"Kumar","year":"2016","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-180764_ref21","doi-asserted-by":"crossref","unstructured":"L.\u00a0Lamport, How to write a proof, in: Global Analysis in Modern Mathematics, 1993, pp.\u00a0311\u2013321. Also published in American Mathematical Monthly 102(7) (1995), 600\u2013608.","DOI":"10.1080\/00029890.1995.12004627"},{"issue":"1","key":"10.3233\/AIC-180764_ref22","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s11784-012-0071-6","article-title":"How to write a 21st century proof","volume":"11","author":"Lamport","year":"2012","journal-title":"Journal of Fixed Point Theory and Applications"},{"key":"10.3233\/AIC-180764_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1754-0_3"},{"key":"10.3233\/AIC-180764_ref25","doi-asserted-by":"crossref","unstructured":"N.D.\u00a0Megill, Metamath: A Computer Language for Pure Mathematics, Lulu Press, Morrisville, NC, 2007, http:\/\/us.metamath.org\/downloads\/metamath.pdf.","DOI":"10.1007\/11542384_13"},{"key":"10.3233\/AIC-180764_ref26","doi-asserted-by":"crossref","unstructured":"R.\u00a0Milner, LCF: A way of doing proofs with a machine, in: Mathematical Foundations of Computer Science 1979, J.\u00a0Be\u010dv\u00e1\u0159, ed., Springer, Berlin, 1979, pp.\u00a0146\u2013159. ISBN 978-3-540-35088-0.","DOI":"10.1007\/3-540-09526-8_11"},{"key":"10.3233\/AIC-180764_ref27","doi-asserted-by":"crossref","unstructured":"R.\u00a0Milner, M.\u00a0Tofte and D.\u00a0Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"10.3233\/AIC-180764_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9452-5"},{"key":"10.3233\/AIC-180764_ref29","doi-asserted-by":"crossref","unstructured":"T.\u00a0Nipkow, L.C.\u00a0Paulson and M.\u00a0Wenzel, Isabelle\/HOL \u2013 A\u00a0Proof Assistant for Higher-Order Logic, LNCS, Vol.\u00a02283, Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"issue":"1","key":"10.3233\/AIC-180764_ref30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-015-9322-8","article-title":"A mechanised proof of G\u00f6del\u2019s incompleteness theorems using Nominal Isabelle","volume":"55","author":"Paulson","year":"2015","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"10.3233\/AIC-180764_ref31","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF02432151","article-title":"Seventy-five problems for testing automatic theorem provers","volume":"2","author":"Pelletier","year":"1986","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-180764_ref35","doi-asserted-by":"crossref","unstructured":"T.\u00a0Ridge and J.\u00a0Margetson, A mechanically verified, sound and complete theorem prover for first order logic, in: TPHOL\u2019s 2005, J.\u00a0Hurd and T.\u00a0Melham, eds, LNCS, Vol.\u00a03603, Springer, 2005, pp.\u00a0294\u2013309.","DOI":"10.1007\/11541868_19"},{"key":"10.3233\/AIC-180764_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_21"},{"issue":"3","key":"10.3233\/AIC-180764_ref38","doi-asserted-by":"crossref","first-page":"199","DOI":"10.2478\/v10037-012-0023-z","article-title":"The G\u00f6del completeness theorem for uncountable languages","volume":"20","author":"Schl\u00f6der","year":"2012","journal-title":"Formalized Mathematics"},{"issue":"3","key":"10.3233\/AIC-180764_ref39","doi-asserted-by":"publisher","first-page":"602","DOI":"10.2307\/2272910","article-title":"A simplified formalization of predicate logic with identity","volume":"39","author":"Tarski","year":"1974","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"10.3233\/AIC-180764_ref40","first-page":"55","article-title":"NaDeA: A\u00a0natural deduction assistant with a formalization in Isabelle","volume":"4","author":"Villadsen","year":"2017","journal-title":"IfCoLog Journal of Logics and their Applications"},{"key":"10.3233\/AIC-180764_ref41","doi-asserted-by":"crossref","unstructured":"M.\u00a0Wenzel, Isar \u2013 A generic interpretative approach to readable formal proof documents, in: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u201999, Proceedings, Nice, France, September 14\u201317, 1999, Springer, 1999, pp.\u00a0167\u2013184.","DOI":"10.1007\/3-540-48256-3_12"},{"key":"10.3233\/AIC-180764_ref42","doi-asserted-by":"crossref","unstructured":"M.\u00a0Wenzel, System description: Isabelle\/jEdit in 2014, in: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, July 17, 2014, Electronic Proceedings in Theoretical Computer Science, Vol.\u00a0167, 2014, pp.\u00a084\u201394.","DOI":"10.4204\/EPTCS.167.10"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-180764","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,10]],"date-time":"2025-03-10T22:23:37Z","timestamp":1741645417000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-180764"}},"subtitle":[],"editor":[{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"short-title":[],"issued":{"date-parts":[[2018,5,17]]},"references-count":32,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.3233\/aic-180764","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"type":"electronic","value":"1875-8452"},{"type":"print","value":"0921-7126"}],"subject":[],"published":{"date-parts":[[2018,5,17]]}}}