MPTP-motivation, implementation, first experiments

DOI10.1007/s10817-004-6245-1zbMath1075.68081OpenAlexW2064800569MaRDI QIDQ556682

Josef Urban

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

zbMATH Keywords

ATPMizarMPAMPTP

Mathematics Subject Classification ID

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

• TPTP
• MoMM
• Mizar
• E Theorem Prover

Cites Work

• The TPTP problem library. CNF release v1. 2. 1
• Solution of the Robbins problem
• OSCAR
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item