Pages that link to "Item:Q877826"
From MaRDI portal
The following pages link to MPTP 0.2: Design, implementation, and initial experiments (Q877826):
Displaying 44 items.
- MPTP 0.2 (Q15128) (← links)
- 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)
- 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)
- 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)
- 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)
- 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)
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (Q3541708) (← links)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance (Q3541722) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← 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)
- Hierarchical invention of theorem proving strategies (Q5145434) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Sine Qua Non for Large Theory Reasoning (Q5200032) (← links)
- Licensing the Mizar Mathematical Library (Q5200114) (← links)
- Sledgehammer: Judgement Day (Q5747754) (← links)
- Hammering Mizar by Learning Clause Guidance (Short Paper). (Q5875448) (← links)
- Solving hard Mizar problems with instantiation and strategy invention (Q6648179) (← links)
- Invariant neural architecture for learning term synthesis in instantiation proving (Q6650564) (← links)
- Graph sequence learning for premise selection (Q6650565) (← links)
