Show simple item record

dc.contributor.authorKoutsoukou-Argyraki, Angeliki
dc.date.accessioned2021-01-21T17:24:38Z
dc.date.available2021-01-21T17:24:38Z
dc.date.issued2020-10-06
dc.identifier.issn0012-0456
dc.identifier.others13291-020-00221-1
dc.identifier.other221
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/316551
dc.description.abstractAbstract: 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.
dc.languageen
dc.publisherSpringer Berlin Heidelberg
dc.rightsAttribution 4.0 International (CC BY 4.0)en
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/en
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-01-21T17:24:37Z
prism.endingPage26
prism.issueIdentifier1
prism.publicationNameJahresbericht der Deutschen Mathematiker-Vereinigung
prism.startingPage3
prism.volume123
dc.identifier.doi10.17863/CAM.63660
rioxxterms.versionofrecord10.1365/s13291-020-00221-1
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/
dc.identifier.eissn1869-7135


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International (CC BY 4.0)
Except where otherwise noted, this item's licence is described as Attribution 4.0 International (CC BY 4.0)