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.
Jamnik have previously applied an Inductive Logic Programming technique to examples of proofs in the @math mega system @cite_6 . Given a collection of well chosen proof method sequences, Jamnik perform a method of least generalisation to infer what are ultimately regular grammars. The value of even basic models is intuitive. Proofs could be derived automatically using the technique. However, the proof steps learned do not contain any parameters. The parameters required are reconstructed after running the learning technique.
@cite_6
2063371232
In this paper we present an approach to automated learning within mathematical reasoning systems. In particular, the approach enables proof planning systems to automatically learn new proof methods from well-chosen examples of proofs which use a similar reasoning pattern to prove related theorems. Our approach consists of an abstract representation for methods and a machine learning technique which can learn methods using this representation formalism. We present an implementation of the approach within the mega proof planning system, which we call Learnma tic. We also present the results of the experiments that we ran on this implementation in order to evaluate if and how it improves the power of proof planning systems.