PRocH

MaRDI QIDQ22158swMATHFDO

Official website http://link.springer.com/chapter/10.1007/978-3-642-38574-2_18

Described by source

• PRocH: proof reconstruction for HOL Light

Cited in

(14)

• Semi-intelligible Isar proofs from machine-generated proofs
• Automated Improving of Proof Legibility in the Mizar System
• AGORA
• Network Security Policy Verification
• Regular_Algebras
• MizAR 40 for Mizar 40
• Automated reasoning service for HOL Light
• Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted theorem proving with millions of lemmas
• Formal mathematics on display: a wiki for Flyspeck
• Hammer for Coq: automation for dependent type theory
• A vernacular for coherent logic
• Hammering towards QED

This page was built for software: PRocH