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

Download (3MB)
Preview



Postscript
Language: English 

Download (1MB)
Preview



Official URL http://www.cs.kent.ac.uk/pubs/1999/909 
Abstract
It is possible to implement mathematical proofs in a machinereadable language. Indeed, certain proofs, especially those deriving properties of safetycritical 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 firstorder 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:  Faculties > Sciences > School of Computing > Theoretical Computing Group 
Depositing User:  Mark Wheadon 
Date Deposited:  20 Oct 2009 12:31 UTC 
Last Modified:  28 May 2019 14:01 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/21861 (The current URI for this page, for reference purposes) 
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):