Semi-intelligible Isar Proofs from Machine-Generated Proofs

Autor: Mathias Fleury, Sascha Böhme, Steffen Smolka, Jasmin Christian Blanchette, Albert Steckermeier

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2016, ⟨10.1007/s10817-015-9335-3⟩
Journal of Automated Reasoning, 2016, ⟨10.1007/s10817-015-9335-3⟩

International audience; Sledgehammer is a component of the Isabelle/HOL proof assistant that integrates external automatic theorem provers (ATPs) to discharge interactive proof obligations. As a safeguard against bugs, the proofs found by the externa

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a313303b9bebaf8670ad0525bdd51120
https://hal.inria.fr/hal-01211748