Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/40814
Title: Automating Proofs with State Machine Inference
Authors: Gransden, Thomas Glenn
Supervisors: Walkinshaw, Neil
Raman, Rajeev
First Published: 14-Dec-2017
Award date: 14-Dec-2017
Abstract: Interactive theorem provers are tools that help to produce formal proofs in a semiautomatic fashion. Originally designed to verify mathematical statements, they can be potentially useful in an industrial context. Despite being endorsed by leading mathematicians and computer scientists, these tools are not widely used. This is mainly because constructing proofs requires a large amount of human effort and knowledge. Frustratingly, there is limited proof automation available in many theorem proving systems. To address this limitation, a new technique called SEPIA (Search for Proofs Using Inferred Automata) is introduced. There are typically large libraries of completed proofs available. However, identifying useful information from these can be difficult and time-consuming. SEPIA uses state-machine inference techniques to produce descriptive models from corpora of Coq proofs. The resulting models can then be used to automatically generate proofs. Subsequently, SEPIA is also combined with other approaches to form an intelligent suite of methods (called Coq-PR3) to help automatically generate proofs. All of the techniques presented are available as extensions for the ProofGeneral interface. In the experimental work, the new techniques are evaluated on two large Coq datasets. They are shown to prove more theorems automatically than compared to existing proof automation. Additionally, various aspects of the discovered proofs are explored, including a comparison between the automatically generated proofs and manually created ones. Overall, the techniques are demonstrated to be a potentially useful addition to the proof development process because of their ability to automate proofs in Coq.
Links: http://hdl.handle.net/2381/40814
Type: Thesis
Rights: Copyright © the author. All rights reserved.
Appears in Collections:Leicester Theses
Theses, Dept. of Informatics

Files in This Item:
File Description SizeFormat 
2017GransdenTGPhD.pdfThesis1.15 MBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.