PRocH: proof reconstruction for HOL Light

DOI10.1007/978-3-642-38574-2_18MaRDI QIDQ4928443zbMATH OpenOpenAlexWikidataFDO

Authors Cezary Kaliszyk, Josef Urban

Publication date 14 June 2013

Published in Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38574-2_18

Mathematics Subject Classification ID

Recommendations

• Proofs and reconstructions
• Scalable LCF-style proof translation
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Automated reasoning service for HOL Light
• scientific article; zbMATH DE number 2185701

Cites work

• Ivy

Cited in

(17)

• On the two definitions of Ho(pro C)
• Hammer for Coq: automation for dependent type theory
• HOL(y)Hammer: online ATP service for HOL Light
• Reliable reconstruction of fine-grained proofs in a proof assistant
• PRocH
• Capturing hiproofs in HOL light
• MizAR 40 for Mizar 40
• Lemma Mining over HOL Light
• Semi-intelligible Isar proofs from machine-generated proofs
• Proofs and reconstructions
• scientific article; zbMATH DE number 2185701 (Why is no real title available?)
• Learning-assisted theorem proving with millions of lemmas
• Scalable LCF-style proof translation
• Steps towards Verified Implementations of HOL Light
• Automated Improving of Proof Legibility in the Mizar System
• A vernacular for coherent logic
• scientific article; zbMATH DE number 7594146 (Why is no real title available?)

Describes a project that uses

Uses Software

• Ivy
• HOL Light
• Metis
• Sledgehammer
• Flyspeck
• TPTP

This page was built for publication: PRocH: proof reconstruction for HOL Light

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928443)