Skip to main content
Kent Academic Repository

On the Readability of Machine Checkable Formal Proofs

Zammit, Vincent (1999) On the Readability of Machine Checkable Formal Proofs. Doctor of Philosophy (PhD) thesis, UNSPECIFIED. (KAR id:21861)

PDF
Language: English
Download this file
(PDF/1MB)
[thumbnail of on_the_readability_of_machine_checkable_zammit.pdf]
Preview
Postscript
Language: English
Download this file
(Postscript/1MB)
[thumbnail of on_the_readability_of_machine_checkable_zammit.ps]
Preview
Official URL:
http://www.cs.kent.ac.uk/pubs/1999/909

Abstract

It is possible to implement mathematical proofs in a machine-readable language. Indeed, certain proofs, especially those deriving properties of safety-critical systems, are often required to be checked by machine in order to avoid human errors. However, machine checkable proofs are very hard to follow by a human reader. Because of their unreadability, such proofs are hard to implement, and more difficult still to maintain and modify. In this thesis we study the possibility of implementing machine checkable proofs in a more readable format. We design a declarative proof language, SPL, which is based on the Mizar language. We also implement a proof checker for SPL which derives theorems in the HOL system from SPL proof scripts. The language and its proof checker are extensible, in the sense that the user can modify and extend the syntax of the language and the deductive power of the proof checker during the mechanisation of a theory. A deductive database of trivial knowledge is used by the proof checker to derive facts which are considered trivial by the developer of mechanised theories so that the proofs of such facts can be omitted. We also introduce the notion of structured straightforward justifications, in which simple facts, or conclusions, are justified by a number of premises together with a number of inferences which are used in deriving the conclusion from the given premises. A tableau prover for first-order logic with equality is implemented as a HOL derived rule and used during the proof checking of SPL scripts. The work presented in this thesis also includes a case study involving the mechanisation of a number of results in group theory in SPL, in which the deductive power of the SPL proof checker is extended throughout the development of the theory.

Item Type: Thesis (Doctor of Philosophy (PhD))
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: Mark Wheadon
Date Deposited: 20 Oct 2009 12:31 UTC
Last Modified: 16 Nov 2021 10:00 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21861 (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.