PRocH

swMATH10191MaRDI QIDQ22158FDOQ22158

Author name not available (Why is that?)

Described by source

• PRocH: proof reconstruction for HOL Light

Cited In (11)

• Semi-intelligible Isar proofs from machine-generated proofs
• Automated Improving of Proof Legibility in the Mizar System
• 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
• A vernacular for coherent logic
• Hammer for Coq: automation for dependent type theory
• Hammering towards QED

This page was built for software: PRocH