MPTP-motivation, implementation, first experiments
From MaRDI portal
Publication:556682
DOI10.1007/s10817-004-6245-1zbMath1075.68081OpenAlexW2064800569MaRDI QIDQ556682
Publication date: 22 June 2005
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-004-6245-1
Related Items
MizAR 40 for Mizar 40 ⋮ Mizar: State-of-the-art and Beyond ⋮ System Description: E.T. 0.1 ⋮ MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Hammer for Coq: automation for dependent type theory ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ Random Forests for Premise Selection ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Hierarchical invention of theorem proving strategies ⋮ Integrating searching and authoring in Mizar ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ Extracting Higher-Order Goals from the Mizar Mathematical Library ⋮ Towards the automatic mathematician ⋮ MPTP ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Presenting and Explaining Mizar ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Premise selection for mathematics by corpus analysis and kernel methods
Uses Software
Cites Work
