PRocH: Proof Reconstruction for HOL Light

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

Josef Urban, Cezary Kaliszyk

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

Cites Work

• Ivy

Cited In (13)

• 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
• Title not available (Why is that?)
• PRocH
• MizAR 40 for Mizar 40
• A Vernacular for Coherent Logic
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted theorem proving with millions of lemmas
• Hammer for Coq: automation for dependent type theory
• 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)