MPTP 0.2: Design, implementation, and initial experiments
From MaRDI portal
Recommendations
Cites work
- A Brief History of Natural Deduction
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 1951634 (Why is no real title available?)
- scientific article; zbMATH DE number 1951639 (Why is no real title available?)
- scientific article; zbMATH DE number 1951640 (Why is no real title available?)
- scientific article; zbMATH DE number 1507187 (Why is no real title available?)
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19--21, 2004. Proceedings.
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP-motivation, implementation, first experiments
- On equivalents of well-foundedness. An experiment in MIZAR
- On the rules of suppositions in formal logic
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Superposition with equivalence reasoning and delayed clause normal form transformation.
- The TPTP problem library. CNF release v1. 2. 1
Cited in
(59)- MPTP 0.2
- Aligning concepts across proof assistant libraries
- The role of the Mizar mathematical library for interactive proof development in Mizar
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Eliciting implicit assumptions of Mizar proofs by property omission
- ATP and presentation service for Mizar formalizations
- The Mizar Mathematical Library in OMDoc: translation and applications
- Improving stateful premise selection with transformers
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- Eliminating models during model elimination
- Learning theorem proving components
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- JGXYZ: an ATP system for gap and glut logics
- Semantics of Mizar as an Isabelle object logic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- scientific article; zbMATH DE number 1614711 (Why is no real title available?)
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Presenting and explaining Mizar
- MizAR 40 for Mizar 40
- Encoding monomorphic and polymorphic types
- MaLeCoP. Machine learning connection prover
- A learning-based fact selector for Isabelle/HOL
- Mining the Archive of Formal Proofs
- Mizar: state-of-the-art and beyond
- System description: E.T. 0.1
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- scientific article; zbMATH DE number 1507187 (Why is no real title available?)
- Theorem proving in large formal mathematics as an emerging AI field
- MPTP 0.1 -- system description
- Make E Smart Again (Short Paper)
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Prolog Technology Reinforcement Learning Prover
- Proceedings of the seventh workshop on proof eXchange for theorem proving, Pittsburg, USA, July 11, 2021
- Hierarchical invention of theorem proving strategies
- Extending Sledgehammer with SMT solvers
- Sine qua non for large theory reasoning
- Licensing the Mizar Mathematical Library (MML)
- MPTP-motivation, implementation, first experiments
- Sledgehammer: judgement day
- Evaluation of automated theorem proving on the Mizar mathematical library
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- VizAR: visualization of automated reasoning proofs (system description)
- Initial experiments with TPTP-style automated theorem provers on ACL2 problems
- Solving hard Mizar problems with instantiation and strategy invention
- Invariant neural architecture for learning term synthesis in instantiation proving
- Graph sequence learning for premise selection
- Machine learning for quantifier selection in cvc5
- Stateful premise selection by recurrent neural networks
- Learning guided automated reasoning: a brief survey
- An empirical assessment of progress in automated theorem proving
- JEFL: joint embedding of formal proof libraries
- Fast and slow enigmas and parental guidance
- Vampire with a brain is a good ITP hammer
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
This page was built for publication: MPTP 0.2: Design, implementation, and initial experiments
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q877826)
