Automated reasoning service for HOL Light

DOI10.1007/978-3-642-39320-4_8zbMATH Open1390.68576OpenAlexW2102819792WikidataQ108482172 ScholiaQ108482172MaRDI QIDQ2843009FDOQ2843009

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

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

Mathematics Subject Classification ID

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

Uses Software

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

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)