MPTP

swMATH2489MaRDI QIDQ15028

No author found.

Described by source

• MPTP-motivation, implementation, first experiments

Related Items (25)

MizAR 40 for Mizar 40 ⋮ ATP-based cross-verification of Mizar proofs: method, systems, and first experiments ⋮ 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 ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ A neurally-guided, parallel theorem prover ⋮ ATP Cross-Verification of the Mizar MPTP Challenge Problems ⋮ Random Forests for Premise Selection ⋮ MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Hierarchical invention of theorem proving strategies ⋮ Integrating searching and authoring in Mizar ⋮ TacticToe: Learning to Reason with HOL4 Tactics ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ MPTP 0.1 - System Description ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ Extracting Higher-Order Goals from the Mizar Mathematical Library ⋮ Mathematical Knowledge Management ⋮ 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

This page was built for software: MPTP