Skip to main content
Kent Academic Repository

Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation

Kumar, Ramana, Arthan, Rob, Myreen, Magnus O., Owens, Scott (2016) Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation. Journal of Automated Reasoning, 56 (3). pp. 221-259. ISSN 0168-7433. E-ISSN 1573-0670. (doi:10.1007/s10817-015-9357-x) (KAR id:45155)

PDF Publisher pdf
Language: English


Download this file
(PDF/604kB)
[thumbnail of Owens OA.pdf]
Preview
Request a format suitable for use with assistive technology e.g. a screenreader
PDF Author's Accepted Manuscript
Language: English

Restricted to Repository staff only
[thumbnail of paper.pdf]
Official URL:
http://dx.doi.org/10.1007/s10817-015-9357-x

Abstract

We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison’s verification of the inference system without definitions. Soundness of the logic extends to soundness of a theorem prover, because we also show that a synthesised implementation of the kernel in CakeML refines the inference system. Apart from adding support for definitions and synthesising an implementation, we improve on Harrison’s work by making our model of HOL parametric on the universe of sets, and we prove soundness for an improved principle of constant specification in the hope of encouraging its adoption. Our semantics supports defined constants directly via a context, and we find this approach cleaner than our previous work formalising Wiedijk’s Stateless HOL.

Item Type: Article
DOI/Identification number: 10.1007/s10817-015-9357-x
Uncontrolled keywords: HOL, Higher-order logic, Verification, Interactive theorem proving, Theorem proving, Consistency, Semantics, Self-formalisation, Self-verification
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Scott Owens
Date Deposited: 19 Aug 2015 08:05 UTC
Last Modified: 17 Aug 2022 12:20 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/45155 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.