HackerPapers

arXiv:1505.07987cs.LO

SEPIA: Search for Proofs Using Inferred Automata

Thomas Gransden, Neil Walkinshaw, Rajeev Raman

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
To appear at 25th International Conference on Automated Deduction
Journal reference
DOI
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Sep 2018 to Sep 2018.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Titans of Mathematics Clash Over Epic Proof of ABC Conjecture 1 comment

    • Possibly this? http://www.macs.hw.ac.uk/~ek19/ML4PG/ It's mostly in maintenance mode (at least, I seem to have inherited its maintenance; and it's such a horrible mess of Emacs Lisp + Matlab + shell scripts that I don't dare touch it unless asked ;) ). It's used for clustering…

      chriswarboView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.