SEPIA: Search for Proofs Using Inferred Automata
Logic in Computer Science
2015-06-01 v1
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.
Keywords
Cite
@article{arxiv.1505.07987,
title = {SEPIA: Search for Proofs Using Inferred Automata},
author = {Thomas Gransden and Neil Walkinshaw and Rajeev Raman},
journal= {arXiv preprint arXiv:1505.07987},
year = {2015}
}
Comments
To appear at 25th International Conference on Automated Deduction