HOL Light QE

DOI10.1007/978-3-319-94821-8_13OpenAlexW2963485651MaRDI QIDQ1791161

Patrick Laskowski, Jacques Carette, William M. Farmer

Publication date: 4 October 2018

Full work available at URL: https://arxiv.org/abs/1802.00405

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

The \textsc{MetaCoq} project ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ HOL Light QE

Uses Software

• ACL2
• Coq
• Theorema
• MetaPRL
• HOL
• HOL Light
• Nuprl
• Agda
• HOL2P
• reFLect

This page was built for publication: HOL Light QE