SEPIA: Search for Proofs Using Inferred Automata

DOI10.1007/978-3-319-21401-6_16zbMath1465.68284arXiv1505.07987OpenAlexW1581101260MaRDI QIDQ3454097

Neil Walkinshaw, Rajeev Raman, Thomas Gransden

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

model inferenceinteractive theorem provingproof automation

Mathematics Subject Classification ID

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

Related Items

ENIGMA: efficient learning-based inference guiding machine ⋮ Proof mining with dependent types ⋮ Hammer for Coq: automation for dependent type theory ⋮ CoProver: a recommender system for proof construction ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ TacticToe: learning to prove with tactics ⋮ SEPIA

Uses Software

• Coq
• Isabelle/HOL
• ML4PG

Cites Work

• Unnamed Item
• 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
• Automated and Human Proofs in General Mathematics: An Initial Comparison
• Automatic Learning of Proof Methods in Proof Planning
• Mining State-Based Models from Proof Corpora