Automated Reasoning Service for HOL Light

DOI10.1007/978-3-642-39320-4_8zbMath1390.68576OpenAlexW2102819792WikidataQ108482172 ScholiaQ108482172MaRDI QIDQ2843009

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

Related Items

MizAR 40 for Mizar 40, The 11th IJCAR automated theorem proving system competition – CASC-J11, Learning-assisted theorem proving with millions of lemmas, HOL(y)Hammer: online ATP service for HOL Light

Uses Software

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