Machine Learner for Automated Reasoning 0.4 and 0.5
作者： Jiří Vyskočil , Josef Urban , Cezary Kaliszyk
DOI:
关键词: Reasoning system 、 Computer science 、 Mathematical proof 、 Competition (economics) 、 Conjecture 、 Automated reasoning 、 Margin (machine learning) 、 Artificial intelligence 、 Theoretical computer science
摘要: Machine Learner for Automated Reasoning (MaLARea) is a learning and reasoning system proving in large formal libraries where thousands of theorems are available when attacking new conjecture, number related problems proofs can be used to learn specific theorem-proving knowledge. The last version the has by margin won 2013 CASC LTB competition. This paper describes motivation behind methods MaLARea, discusses general approach issues arising evaluation such system, Mizar@Turing100 CASC'24 versions MaLARea.
harvard.edu
arxiv.org参考文章(17)
Kryštof Hoder, Andrei Voronkov, Sine Qua non for large theory reasoning conference on automated deduction. pp. 299- 314 ,(2011) , 10.1007/978-3-642-22438-6_23
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban, MaSh: Machine Learning for Sledgehammer Interactive Theorem Proving. pp. 35- 50 ,(2013) , 10.1007/978-3-642-39634-2_6
Daniel Kühlwein, Josef Urban, Learning from Multiple Proofs: First Experiments international joint conference on automated reasoning. pp. 82- 94 ,(2012)
Josef Urban, MaLARea: a Metasystem for Automated Reasoning in Large Theories. ESARLT. ,(2007)
Nello Cristianini, John Shawe-Taylor, Kernel Methods for Pattern Analysis ,(2004)
Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jiří Vyskočil, MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance international joint conference on automated reasoning. pp. 441- 456 ,(2008) , 10.1007/978-3-540-71070-7_37
Stephan Schulz, E - a brainiac theorem prover Ai Communications. ,vol. 15, pp. 111- 126 ,(2002)
Cezary Kaliszyk, Josef Urban, Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution Blanchette, J. (ed.), Pxtp 2013. Third international workshop on proof exchange for theorem proving. ,vol. 14, pp. 87- 95 ,(2013) , 10.29007/5GZR
Daniel Kühlwein, Tom Heskes, Jesse Alama, Josef Urban, Evgeni Tsivtsivadze, Premise Selection for Mathematics by Corpus Analysis and Kernel Methods Journal of Automated Reasoning. ,vol. 52, pp. 191- 213 ,(2014) , 10.1007/S10817-013-9286-5
Josef Urban, MPTP 0.2: Design, Implementation, and Initial Experiments Journal of Automated Reasoning. ,vol. 37, pp. 21- 43 ,(2006) , 10.1007/S10817-006-9032-3