PRocH: Proof Reconstruction for HOL Light. PRocH is a proof reconstruction tool that imports in HOL Light proofs produced by ATPs on the recently developed translation of HOL Light and Flyspeck problems to ATP formats. PRocH combines several reconstruction methods in parallel, but the core improvement over previous methods is obtained by re-playing in the HOL logic the detailed inference steps recorded in the ATP (TPTP) proofs, using several internal HOL Light inference methods. These methods range from fast variable matching and more involved rewriting, to full first-order theorem proving using the MESON tactic. The system is described and its performance is evaluated here on a large set of Flyspeck problems.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
- Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
- Pąk, Karol: Automated improving of proof legibility in the Mizar system (2014)
- Stojanović, Sana; Narboux, Julien; Bezem, Marc; Janičić, Predrag: A vernacular for coherent logic (2014)
- Bonacina, Maria Paola (ed.): Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings (2013)
- Kaliszyk, Cezary; Urban, Josef: Automated reasoning service for HOL Light (2013)
- Kaliszyk, Cezary; Urban, Josef: PRocH: proof reconstruction for HOL Light (2013)
- Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman: Formal mathematics on display: a wiki for Flyspeck (2013)