Please use this identifier to cite or link to this item:
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
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
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.