PRocH: proof reconstruction for HOL Light
From MaRDI portal
Publication:4928443
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
Cites Work
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
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)