SEPIA: search for proofs using inferred automata

DOI10.1007/978-3-319-21401-6_16zbMATH Open1465.68284arXiv1505.07987OpenAlexW1581101260MaRDI QIDQ3454097FDOQ3454097

Authors: Thomas Gransden, Neil Walkinshaw, Rajeev Raman 

Publication date: 2 December 2015

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

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.

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

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

zbMATH Keywords

interactive theorem provingproof automationmodel inference

Mathematics Subject Classification ID

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

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Automated and human proofs in general mathematics: an initial comparison
• Title not available (Why is that?)
• Automatic Learning of Proof Methods in Proof Planning
• 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
• Title not available (Why is that?)
• 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

Uses Software

• Coq
• Isabelle/HOL
• ML4PG

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)