Pages that link to "Item:Q556682"

The following pages link to MPTP-motivation, implementation, first experiments (Q556682):

Displaying 22 items.

• MPTP (Q15028) (← links)
• MizAR 40 for Mizar 40 (Q286800) (← links)
• Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics (Q865631) (← links)
• MPTP 0.2: Design, implementation, and initial experiments (Q877826) (← links)
• The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
• Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
• TacticToe: learning to prove with tactics (Q2031416) (← links)
• Machine learning guidance for connection tableaux (Q2031418) (← links)
• Towards the automatic mathematician (Q2055841) (← 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)
• Integrating searching and authoring in Mizar (Q2462640) (← links)
• Extracting Higher-Order Goals from the Mizar Mathematical Library (Q2817297) (← links)
• Presenting and Explaining Mizar (Q2867936) (← links)
• Random Forests for Premise Selection (Q2964471) (← links)
• Mizar: State-of-the-art and Beyond (Q3453119) (← links)
• System Description: E.T. 0.1 (Q3454109) (← links)
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
• Hierarchical invention of theorem proving strategies (Q5145434) (← links)
• Solving hard Mizar problems with instantiation and strategy invention (Q6648179) (← links)