SEPIA: search for proofs using inferred automata

DOI10.1007/978-3-319-21401-6_16MaRDI QIDQ3454097zbMATH OpenOpenAlexFDO

Authors Thomas Gransden, Neil Walkinshaw, Rajeev Raman

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1505.07987

zbMATH Keywords

interactive theorem provingproof automationmodel inference

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• Mining state-based models from proof corpora
• The Tactician. A seamless, interactive tactic learner and prover for Coq
• How to make ad hoc proof automation less ad hoc
• How to make ad hoc proof automation less ad hoc
• Recycling proof patterns in Coq: case studies

Cites work

• scientific article; zbMATH DE number 5486212 (Why is no real title available?)
• Automated and human proofs in general mathematics: an initial comparison
• Automatic Learning of Proof Methods in Proof Planning
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Mining state-based models from proof corpora

Cited in

(10)

• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Mining state-based models from proof corpora
• TacticToe: learning to prove with tactics
• scientific article; zbMATH DE number 2081040 (Why is no real title available?)
• ENIGMA: efficient learning-based inference guiding machine
• Proof mining with dependent types
• SEPIA
• Learning Proof Transformations and Its Applications in Interactive Theorem Proving
• Hammer for Coq: automation for dependent type theory
• CoProver: a recommender system for proof construction

Describes a project that uses

Uses Software

• ML4PG
• Isabelle/HOL
• Coq

This page was built for publication: SEPIA: search for proofs using inferred automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3454097)