Show simple item record

dc.contributor.authorBenzmüller, Christophen
dc.contributor.authorSultana, Nikolaien
dc.contributor.authorPaulson, Lawrenceen
dc.contributor.authorTheiß, Franken
dc.date.accessioned2015-07-23T08:45:42Z
dc.date.available2015-07-23T08:45:42Z
dc.date.issued2015-09-22en
dc.identifier.citationBenzmüller et al. Journal of Automated Reasoning (2015) Vol. 55, Issue 4, pp. 389-404. doi: 10.1007/s10817-015-9348-yen
dc.identifier.issn0168-7433
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/249011
dc.description.abstractLeo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order-first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic, and it has been applied in a wide array of problems. Leo-II may also be called in proof assistants as an external aid tool to save user effort. For this it is crucial that Leo-II returns proof information in a standardised syntax, so that these proofs can eventually be transformed and verified within proof assistants. Recent progress in this direction is reported for the Isabelle/HOL system.
dc.description.sponsorshipThe Leo-II project has been supported by the following grants: EPSRC grant EP/D070511/1 and DFG grants BE/2501 6-1, 8-1 and 9-1.
dc.languageEnglishen
dc.language.isoenen
dc.publisherSpringer
dc.rightsAttribution 4.0 UK: England & Wales
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/uk/
dc.titleThe Higher-Order Prover Leo-IIen
dc.typeArticle
dc.description.versionThis is the final version of the article. It first appeared from Springer via http://dx.doi.org/10.1007/s10817-015-9348-y.en
prism.endingPage404
prism.publicationDate2015en
prism.publicationNameJournal of Automated Reasoningen
prism.startingPage389
prism.volume55en
dc.rioxxterms.funderEPSRC
dc.rioxxterms.projectidEP/D070511/1
dcterms.dateAccepted2015-09-04en
rioxxterms.versionofrecord10.1007/s10817-015-9348-yen
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2015-09-22en
dc.contributor.orcidPaulson, Lawrence [0000-0003-0288-4279]
dc.identifier.eissn1573-0670
rioxxterms.typeJournal Article/Reviewen
pubs.funder-project-idEPSRC (EP/I011005/1)
pubs.funder-project-idEPSRC (EP/D070511/1)
rioxxterms.freetoread.startdate2050-01-01


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 UK: England & Wales
Except where otherwise noted, this item's licence is described as Attribution 4.0 UK: England & Wales