MPTP 0.2
From MaRDI portal
swMATH2589MaRDI QIDQ15128FDOQ15128
Author name not available (Why is that?)
Official website: https://github.com/JUrban/MPTP2
Source code repository: https://github.com/JUrban/MPTP2
Cited In (99)
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Presenting and explaining Mizar
- Improving stateful premise selection with transformers
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- Eliminating models during model elimination
- Learning theorem proving components
- HOList
- Semantics of Mizar as an Isabelle object logic
- Make E Smart Again (Short Paper)
- Prolog Technology Reinforcement Learning Prover
- Detecting inconsistencies in large first-order knowledge bases
- Extending Sledgehammer with SMT solvers
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Fast and slow enigmas and parental guidance
- JEFL: joint embedding of formal proof libraries
- Vampire with a brain is a good ITP hammer
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- TPTP, TSTP, CASC, etc.
- Aligning concepts across proof assistant libraries
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Mining the Archive of Formal Proofs
- Deep network guided proof search
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- The Mizar Mathematical Library in OMDoc: translation and applications
- Title not available (Why is that?)
- The role of the Mizar mathematical library for interactive proof development in Mizar
- MizarMode
- MPTP
- VAMPIRE
- gensim
- MoMM
- Mizar
- LPL software
- MML
- MaLeCoP
- E-MaLeS 1.1
- Polar
- MaSh
- Tipi
- ileanCoP
- DLog
- leanCoP
- E Theorem Prover
- Flyspeck
- MaLARea
- SystemOnTPTP
- HOLyHammer
- Easychair
- Metamath
- SMTtoTPTP
- E-MaLeS
- randoCoP
- SigmaKEE
- Encoding monomorphic and polymorphic types
- SInE
- BliStr
- MizAR 40 for Mizar 40
- System description: E.T. 0.1
- A learning-based fact selector for Isabelle/HOL
- Automated reasoning and presentation support for formalizing mathematics in MizAR
- Sledgehammer: judgement day
- Evaluation of automated theorem proving on the Mizar mathematical library
- Sine qua non for large theory reasoning
- Licensing the Mizar Mathematical Library (MML)
- Automated and human proofs in general mathematics: an initial comparison
- BliStrTune
- miz3
- FEMaLeCoP
- IDV
- SEPIA
- SRASS
- ProofTool
- OpenNMT
- DeepMath
- ATPboost
- ENIGMA
- Logic2CNF
- Proofwatch
- Theorem proving in large formal mathematics as an emerging AI field
- MurmurHash
- Encoding monomorphic and polymorphic types
- ATP and presentation service for Mizar formalizations
- First experiments with neural translation of informal to formal mathematics
- Isabelle import infrastructure for the Mizar Mathematical Library
- mizar-items
- A Wiki for Mizar: motivation, considerations, and initial prototype
- Eliciting implicit assumptions of Mizar proofs by property omission
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- lazyCoP
- MaLeCoP. Machine learning connection prover
- Literal Projection for First-Order Logic
- Mizar: state-of-the-art and beyond
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- ProofWatch: watchlist guidance for large theories in E
- Hammering towards QED
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
This page was built for software: MPTP 0.2
