Show simple item record

dc.contributor.authorBUTTERFIELD, ANDREW
dc.contributor.editorShenchao Qinen
dc.date.accessioned2020-01-17T16:37:30Z
dc.date.available2020-01-17T16:37:30Z
dc.date.created15-16 November 2010en
dc.date.issued2010
dc.date.submitted2010en
dc.identifier.citationButterfield, A., Saoithín: A Theorem Prover for UTP, LNCS, Unifying Theories of Programming, Third International Symposium, UTP 2010, Shanghai, China, 15-16 November 2010, Shenchao Qin, 6445, Springer, 2010, 137 - 156en
dc.identifier.otherY
dc.identifier.urihttps://link.springer.com/chapter/10.1007/978-3-642-16690-7_6
dc.identifier.urihttp://hdl.handle.net/2262/91345
dc.description.abstractSaoithín is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and “programs as predicates” style that is prevalent in much of the UTP literature, from the seminal work by Hoare & He [HH98] onwards. This paper describes the key features of the theorem prover, with an emphasis on the underlying foundations, and how these affect the design and implementation choices. These key features include: a formalisation of a UTP Theory; support for common proof strategies; sophisticated goal/law matching ; and user-defined language constructs. A simple theory of designs with some proof extracts is used to illustrate the above features. The theorem prover has been used with undergraduate students and we discuss some of those experiences. The paper then concludes with a discussion of current limitations and planned improvements to the tool.en
dc.format.extent137en
dc.format.extent156en
dc.language.isoenen
dc.publisherSpringeren
dc.relation.ispartofseriesLNCS;6445
dc.rightsYen
dc.subjectTheorem provingen
dc.subjectUnifying theories of programmingen
dc.subjectFree variableen
dc.subjectProof assistanten
dc.subjectLanguage constructen
dc.subjectFoundational worken
dc.titleSaoithín: A Theorem Prover for UTPen
dc.title.alternativeUnifying Theories of Programming, Third International Symposium, UTP 2010en
dc.typeConference Paperen
dc.contributor.sponsorScience Foundation Irelanden
dc.type.supercollectionscholarly_publicationsen
dc.type.supercollectionrefereed_publicationsen
dc.identifier.peoplefinderurlhttp://people.tcd.ie/butrfeld
dc.identifier.rssinternalid68151
dc.rights.ecaccessrightsopenAccess
dc.contributor.sponsorGrantNumber07/RFP/CMSF186en
dc.contributor.sponsorGrantNumber08/RFP/CMS1277en
dc.contributor.sponsorGrantNumber03/CE2/I303-1en


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record