id:"swepub:oai:research.chalmers.se:81ee6d78-7af0-49eb-adf7-9189dfbc6a31"
Sökning: id:"swepub:oai:research.chalmers.se:81ee6d78-7af0-49eb-adf7-9189dfbc6a31" > A verified proof ch...
- 1 av 1
- Föregående post
- Nästa post
- Till träfflistan
- Abrahamsson, Oskar,1986Chalmers tekniska högskola,Chalmers University of Technology (författare)
A verified proof checker for higher-order logic
- Artikel/kapitelEngelska2020
Förlag, utgivningsår, omfång ...
- Elsevier BV,2020
Nummerbeteckningar
- LIBRIS-ID:oai:research.chalmers.se:81ee6d78-7af0-49eb-adf7-9189dfbc6a31
- https://research.chalmers.se/publication/517007URI
- https://doi.org/10.1016/j.jlamp.2020.100530DOI
Kompletterande språkuppgifter
- Språk:engelska
- Sammanfattning på:engelska
Ingår i deldatabas
- SwePubSwePub
Klassifikation
Anmärkningar
- We present a computer program for checking proofs in higher-order logic (HOL) that is verified to accept only valid proofs. The proof checker is defined as functions in HOL and synthesized to CakeML code, and uses the Candle theorem prover kernel to check logical inferences. The checker reads proofs in the OpenTheory article format, which means proofs produced by various HOL proof assistants are supported. The proof checker is implemented and verified using the HOL4 theorem prover, and comes with a proof of soundness. (C) 2020 Elsevier Inc. All rights reserved.
Ämnesord och genrebeteckningar
- NATURVETENSKAP Matematik Geometri hsv//swe
- NATURAL SCIENCES Mathematics Geometry hsv//eng
- NATURVETENSKAP Data- och informationsvetenskap Datavetenskap hsv//swe
- NATURAL SCIENCES Computer and Information Sciences Computer Sciences hsv//eng
- NATURVETENSKAP Matematik Matematisk analys hsv//swe
- NATURAL SCIENCES Mathematics Mathematical Analysis hsv//eng
- Mechanized proof
- Proof checker
- Soundness
- Higher-order logic
Biuppslag (personer, institutioner, konferenser, titlar ...)
- Chalmers tekniska högskola (creator_code:org_t)
Sammanhörande titlar
- Ingår i:Journal of Logical and Algebraic Methods in Programming: Elsevier BV1122352-22082352-2216
Internetlänk
Hitta via bibliotek
- Journal of Logical and Algebraic Methods in Programming (Sök värdpublikationen i LIBRIS)
Till lärosätets databas
- 1 av 1
- Föregående post
- Nästa post
- Till träfflistan
Hitta mer i SwePub
- Av författaren/redakt...
- Abrahamsson, Osk ...
- Om ämnet
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Matematik
- och Geometri
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Data och informa ...
- och Datavetenskap
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Matematik
- och Matematisk analy ...
- Artiklar i publikationen
- Journal of Logic ...
- Av lärosätet
- Chalmers tekniska högskola
Sök utanför SwePub
- Sök vidare i:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - Nationella bibliotekssystem
- LIBRIS.kb.se
