SEPIA swMATH ID: 21585 Software Authors: Gransden, T., Walkinshaw, N., Raman, R. Description: SEPIA: search for proofs using inferred automata. 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. Homepage: https://link.springer.com/chapter/10.1007%2F978-3-319-21401-6_16 Related Software: Coq; E Theorem Prover; ML4PG; FEMaLeCoP; Flyspeck; MaLeCoP; HOL; VAMPIRE; Isabelle/HOL; TacticToe; MaLARea; HOL Light; Metis_; IsaPlanner; Isabelle; ENIGMA; DeepMath; BliStrTune; Mizar; CoqHammer Cited in: 7 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year SEPIA: search for proofs using inferred automata. Zbl 1465.68284Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev 2015 all top 5 Cited by 15 Authors 3 Urban, Josef 2 Jakubův, Jan 2 Kaliszyk, Cezary 2 Kumar, Ramana 1 Czajka, Łukasz 1 Gauthier, Thibault 1 Goertzel, Zarathustra Amadeus 1 Gransden, Thomas 1 Heras, Jónathan 1 Komendantskaya, Ekaterina 1 Nagashima, Yutaka 1 Norrish, Michael 1 Raman, Rajeev 1 Schulz, Stephan 1 Walkinshaw, Neil Cited in 1 Serial 2 Journal of Automated Reasoning Cited in 2 Fields 7 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year