Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/32390
Title: SEPIA: Search for Proofs Using Inferred Automata
Authors: Gransden, Thomas
Walkinshaw, Neil
Raman, Rajeev
First Published: 1-Aug-2015
Presented at: 25th International Conference on Automated Deduction (CADE-25), Berlin
Publisher: Springer Verlag (Germany)
Citation: Lecture Notes in Computer Science, 2015, 9195, pp 246-255
Abstract: This paper describes SEPIA, a tool for automated proof generation in Coq. SEPIA combines model inference with interactive theorem proving. Existing proof corpora are modelled using state-based models inferred from tactic sequences. These can then be traversed automatically to identify proofs. The SEPIA system is described and its performance evaluated on three Coq datasets. Our results show that SEPIA provides a useful complement to existing automated tactics in Coq.
DOI Link: 10.1007/978-3-319-21401-6_16
ISSN: 0302-9743
ISBN: 978-3-319-21400-9
Links: http://link.springer.com/chapter/10.1007%2F978-3-319-21401-6_16
http://hdl.handle.net/2381/32390
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Archived with reference to SHERPA/RoMEO and publisher website. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-21401-6_16
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
paper_3.pdfPost-review (final submitted)271.3 kBAdobe PDFView/Open


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