Please use this identifier to cite or link to this item:
Title: Mining state-based models from proof corpora
Authors: Gransden, Thomas
Walkinshaw, Neil
Raman, Rajeev
First Published: Jul-2014
Presented at: International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014.
Publisher: Springer International Publishing
Citation: Proceeding of CICM 2014, Coimbra, Portugal, July 7-11, 2014, Lecture Notes in Computer Science (Intelligent Computer Mathematics) 8543 LNAI, pp. 282-297
Abstract: Interactive theorem provers have been used extensively to reason about various software/hardware systems and mathematical theorems. The key challenge when using an interactive prover is finding a suitable sequence of proof steps that will lead to a successful proof requires a significant amount of human intervention. This paper presents an automated technique that takes as input examples of successful proofs and infers an Extended Finite State Machine as output. This can in turn be used to generate proofs of new conjectures. Our preliminary experiments show that the inferred models are generally accurate (contain few false-positive sequences) and that representing existing proofs in such a way can be very useful when guiding new ones.
DOI Link: 10.1007/978-3-319-08434-3_21
ISSN: 0302-9743
ISBN: 978-3-319-08433-6
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © 2014, Springer International Publishing. Deposited with reference to the publisher’s archiving policy available on the SHERPA/RoMEO website
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
1405.3623v1.pdfPost-review (final submitted)374.59 kBUnknownView/Open

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