Automated reasoning service for HOL Light

DOI10.1007/978-3-642-39320-4_8MaRDI QIDQ2843009zbMATH OpenOpenAlexWikidataFDO

Authors Cezary Kaliszyk, Josef Urban

Publication date 9 August 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39320-4_8

Mathematics Subject Classification ID

Recommendations

• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• ATP and presentation service for Mizar formalizations
• Sharing HOL4 and HOL Light proof knowledge
• HOL Light: An Overview

Cited in

(8)

• Towards Knowledge Management for HOL Light
• Sharing HOL4 and HOL Light proof knowledge
• MizAR 40 for Mizar 40
• HOL(y)Hammer: online ATP service for HOL Light
• Learning-assisted theorem proving with millions of lemmas
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• The 11th IJCAR automated theorem proving system competition – CASC-J11
• PRocH: proof reconstruction for HOL Light

Describes a project that uses

Uses Software

• MaLARea
• PRocH
• E Theorem Prover
• MaLeCoP
• HOL Light
• z3
• Mizar
• MoMM
• Metis
• TPTP
• MetiTarski

This page was built for publication: Automated reasoning service for HOL Light

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843009)