MPTP
From MaRDI portal
Cited in
(75)- ALCOR
- ILTP
- mizar-items
- lazyCoP
- MizarMode
- MPTP 0.2
- VAMPIRE
- gensim
- The role of the Mizar mathematical library for interactive proof development in Mizar
- MoMM
- Mizar
- LPL software
- I-SATCHMO
- MML
- MaLeCoP
- Polar
- MaSh
- TacticToe: learning to prove with tactics
- Machine learning guidance for connection tableaux
- Tipi
- ileanCoP
- A neurally-guided, parallel theorem prover
- DLog
- E Theorem Prover
- Flyspeck
- MaLARea
- SystemOnTPTP
- Semantics of Mizar as an Isabelle object logic
- HOLyHammer
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- Integrating searching and authoring in Mizar
- Easychair
- SMTtoTPTP
- FOOL
- randoCoP
- SigmaKEE
- E-MaLeS
- SInE
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Presenting and explaining Mizar
- MizAR 40 for Mizar 40
- BliStr
- Random forests for premise selection
- miz3
- BliStrTune
- SNARK
- FEMaLeCoP
- SRASS
- IDV
- nanoCoP
- SEPIA
- ProofTool
- Mizar: state-of-the-art and beyond
- System description: E.T. 0.1
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- OpenNMT
- DeepMath
- Logic2CNF
- ATPboost
- TacticToe
- ENIGMA
- Jinja not Java
- TacticToe: learning to reason with HOL4 tactics
- MurmurHash
- Learning-assisted theorem proving with millions of lemmas
- Theorem proving in large formal mathematics as an emerging AI field
- MPTP 0.1 -- system description
- Hierarchical invention of theorem proving strategies
- Mathematical Knowledge Management
- HOList
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP 0.2: Design, implementation, and initial experiments
This page was built for software: MPTP
