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)

• Hammer for Coq: automation for dependent type theory
• 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
• Automated reasoning service for HOL Light
• Formal mathematics on display: a wiki for Flyspeck
• MizAR 40 for Mizar 40
• Semi-intelligible Isar proofs from machine-generated proofs
• AGORA
• Network Security Policy Verification
• Regular_Algebras
• Learning-assisted theorem proving with millions of lemmas
• Hammering towards QED
• Automated Improving of Proof Legibility in the Mizar System
• A vernacular for coherent logic

This page was built for software: PRocH