PRocH: Proof Reconstruction for HOL Light

DOI10.1007/978-3-642-38574-2_18zbMath1381.68271OpenAlexW49696946WikidataQ108482180 ScholiaQ108482180MaRDI QIDQ4928443

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

Related Items (8)

MizAR 40 for Mizar 40 ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Hammer for Coq: automation for dependent type theory ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ PRocH ⋮ Automated Improving of Proof Legibility in the Mizar System ⋮ A Vernacular for Coherent Logic

Uses Software

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

Cites Work

• Ivy

This page was built for publication: PRocH: Proof Reconstruction for HOL Light