The following pages link to MPTP 0.2 (Q15128):
Displaying 50 items.
- MizAR 40 for Mizar 40 (Q286800) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- Fast and slow enigmas and parental guidance (Q831937) (← links)
- Vampire with a brain is a good ITP hammer (Q831938) (← links)
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (Q841684) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) (← links)
- ProofWatch: watchlist guidance for large theories in E (Q1791167) (← links)
- Isabelle import infrastructure for the Mizar Mathematical Library (Q1798961) (← links)
- First experiments with neural translation of informal to formal mathematics (Q1798975) (← links)
- Eliciting implicit assumptions of Mizar proofs by property omission (Q1945901) (← links)
- ATP and presentation service for Mizar formalizations (Q1945905) (← links)
- The Mizar Mathematical Library in OMDoc: translation and applications (Q1945907) (← links)
- Improving stateful premise selection with transformers (Q2128800) (← links)
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (Q2128804) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- Eliminating models during model elimination (Q2142079) (← links)
- Learning theorem proving components (Q2142080) (← links)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- Detecting inconsistencies in large first-order knowledge bases (Q2405258) (← links)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326) (← links)
- Extracting Higher-Order Goals from the Mizar Mathematical Library (Q2817297) (← links)
- Presenting and Explaining Mizar (Q2867936) (← links)
- Automated and Human Proofs in General Mathematics: An Initial Comparison (Q2891438) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- MaLeCoP Machine Learning Connection Prover (Q3010374) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- Mizar: State-of-the-art and Beyond (Q3453119) (← links)
- System Description: E.T. 0.1 (Q3454109) (← links)
- ATP Cross-Verification of the Mizar MPTP Challenge Problems (Q3498492) (← links)
- TPTP, TSTP, CASC, etc. (Q3499763) (← links)
- (Q3515519) (← links)
- Literal Projection for First-Order Logic (Q3532481) (← links)
- Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar (Q3582702) (← links)
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype (Q3582731) (← links)
- Deep Network Guided Proof Search (Q4645728) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
- E-MaLeS 1.1 (Q4928455) (← links)
- Make E Smart Again (Short Paper) (Q5049019) (← links)
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) (Q5049022) (← links)
- Prolog Technology Reinforcement Learning Prover (Q5049033) (← links)
- Hammering towards QED (Q5195271) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Sine Qua Non for Large Theory Reasoning (Q5200032) (← links)
- Licensing the Mizar Mathematical Library (Q5200114) (← links)
