PRocH: proof reconstruction for HOL Light

DOI10.1007/978-3-642-38574-2_18zbMATH Open1381.68271OpenAlexW49696946WikidataQ108482180 ScholiaQ108482180MaRDI QIDQ4928443FDOQ4928443

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

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

Mathematics Subject Classification ID

Cites Work

• Ivy

Cited In (16)

• On the two definitions of Ho(pro C)
• Lemma Mining over HOL Light
• Semi-intelligible Isar proofs from machine-generated proofs
• Automated Improving of Proof Legibility in the Mizar System
• Steps towards Verified Implementations of HOL Light
• Proofs and reconstructions
• Title not available (Why is that?)
• PRocH
• MizAR 40 for Mizar 40
• HOL(y)Hammer: online ATP service for HOL Light
• Capturing hiproofs in HOL light
• Learning-assisted theorem proving with millions of lemmas
• A vernacular for coherent logic
• Hammer for Coq: automation for dependent type theory
• Scalable LCF-style proof translation
• Title not available (Why is that?)

Uses Software

• TPTP
• Metis_
• HOL Light
• Sledgehammer
• Flyspeck
• Ivy

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)