Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
From MaRDI portal
Publication:5747877
DOI10.1007/978-3-642-15582-6_30zbMath1294.68128MaRDI 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
Related Items
Sine Qua Non for Large Theory Reasoning, Licensing the Mizar Mathematical Library, Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization, ATP and presentation service for Mizar formalizations, Machine learning guidance for connection tableaux, Semantics of Mizar as an Isabelle object logic, Premise selection for mathematics by corpus analysis and kernel methods, MaLeCoP Machine Learning Connection Prover, A First Class Boolean Sort in First-Order Theorem Proving and TPTP, System Description: E.T. 0.1
Uses Software