MPTP
From MaRDI portal
Software:15028
swMATH2489MaRDI QIDQ15028FDOQ15028
Author name not available (Why is that?)
Cited In (25)
- A neurally-guided, parallel theorem prover
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Presenting and explaining Mizar
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Mizar: State-of-the-art and Beyond
- Mathematical Knowledge Management
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- TacticToe: Learning to Reason with HOL4 Tactics
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Random Forests for Premise Selection
- MizAR 40 for Mizar 40
- Hierarchical invention of theorem proving strategies
- Learning-assisted theorem proving with millions of lemmas
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP 0.2: Design, implementation, and initial experiments
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- Semantics of Mizar as an Isabelle object logic
- MPTP 0.1 - System Description
- Integrating searching and authoring in Mizar
- System Description: E.T. 0.1
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
This page was built for software: MPTP
