Sökning: id:"swepub:oai:research.chalmers.se:81ee6d78-7af0-49eb-adf7-9189dfbc6a31" >
A verified proof ch...
A verified proof checker for higher-order logic
-
- Abrahamsson, Oskar, 1986 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- Elsevier BV, 2020
- 2020
- Engelska.
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 112
- Relaterad länk:
-
https://research.cha...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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
- 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)
Nyckelord
- Mechanized proof
- Proof checker
- Soundness
- Higher-order logic
Publikations- och innehållstyp
- art (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas