Evaluation of Automated Theorem Proving on the Mizar Mathematical Library

DOI10.1007/978-3-642-15582-6_30zbMath1294.68128OpenAlexW1623704225MaRDI QIDQ5747877

Josef Urban, Andrei Voronkov, Kryštof Hoder

Publication date: 14 September 2010

Published in: Mathematical Software – ICMS 2010 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-15582-6_30

Mathematics Subject Classification ID

Related Items

Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization, A First Class Boolean Sort in First-Order Theorem Proving and TPTP, System Description: E.T. 0.1, ATP and presentation service for Mizar formalizations, MaLeCoP Machine Learning Connection Prover, Machine learning guidance for connection tableaux, Sine Qua Non for Large Theory Reasoning, Licensing the Mizar Mathematical Library, Semantics of Mizar as an Isabelle object logic, Premise selection for mathematics by corpus analysis and kernel methods

Uses Software

• MPTP 0.2
• VAMPIRE
• Mizar
• MML
• E Theorem Prover
• MaLARea