Show simple item record

dc.contributor.authorKoutsoukou-Argyraki, A
dc.date.accessioned2021-10-06T15:47:09Z
dc.date.available2021-10-06T15:47:09Z
dc.date.issued2021-03
dc.identifier.issn1869-7135
dc.identifier.others13291-020-00221-1
dc.identifier.other221
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/329049
dc.description.abstract<jats:title>Abstract</jats:title><jats:p>This is an account of a mathematician’s first experiences with the proof assistant (interactive theorem prover) Isabelle/HOL, including a discussion on the rationale behind formalising mathematics and the choice of Isabelle/HOL in particular, some instructions for new users, some technical and conceptual observations focussing on some of the first difficulties encountered, and some thoughts on the use and potential of proof assistants for mathematics.</jats:p>
dc.languageen
dc.publisherSpringer Fachmedien Wiesbaden GmbH
dc.subjectSurvey Article
dc.subjectInteractive theorem proving
dc.subjectIsabelle/HOL
dc.subjectProof assistant
dc.subjectFormalisation of mathematics
dc.subject03B35
dc.subject68V15
dc.subject68V20
dc.subject68V35
dc.titleFormalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started
dc.typeArticle
dc.date.updated2021-10-06T15:47:08Z
prism.endingPage26
prism.issueIdentifier1
prism.publicationNameJahresbericht der Deutschen Mathematiker-Vereinigung
prism.startingPage3
prism.volume123
dc.identifier.doi10.17863/CAM.76494
rioxxterms.versionofrecord10.1365/s13291-020-00221-1
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/
dc.identifier.eissn0012-0456
pubs.funder-project-idEuropean Research Council (742178)
cam.issuedOnline2020-10-06


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record