Mining State-Based Models from Proof Corpora

DOI10.1007/978-3-319-08434-3_21zbMath1304.68155arXiv1405.3623OpenAlexW1542564959MaRDI QIDQ5495930

Rajeev Raman, Thomas Gransden, Neil Walkinshaw

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

model inferenceinteractive theorem provingextended state machines

Mathematics Subject Classification ID

Related Items

Proof mining with dependent types, SEPIA: Search for Proofs Using Inferred Automata

Uses Software

• ACL2
• Coq
• IsaPlanner
• Metis_
• WEKA
• Sledgehammer
• ML4PG
• MaSh
• Flyspeck
• C4.5

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• MizAR 40 for Mizar 40
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Premise selection for mathematics by corpus analysis and kernel methods
• Translating higher-order clauses to first-order clauses
• ML4PG in Computer Algebra Verification
• A Graphical Language for Proof Strategies
• Proof-Pattern Recognition and Lemma Discovery in ACL2
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Automatic Learning of Proof Methods in Proof Planning
• MaSh: Machine Learning for Sledgehammer
• A Machine-Checked Proof of the Odd Order Theorem
• On the Synthesis of Finite-State Machines from Samples of Their Behavior
• Language identification in the limit
• Sledgehammer: Judgement Day