MPTP 0.2: Design, implementation, and initial experiments
From MaRDI portal
Publication:877826
DOI10.1007/s10817-006-9032-3zbMath1113.68095OpenAlexW1995539874MaRDI QIDQ877826
Publication date: 3 May 2007
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-006-9032-3
Related Items
Improving stateful premise selection with transformers, Heterogeneous heuristic optimisation and scheduling for first-order theorem proving, MizAR 40 for Mizar 40, JEFL: joint embedding of formal proof libraries, Fast and slow enigmas and parental guidance, Vampire with a brain is a good ITP hammer, Make E Smart Again (Short Paper), ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Prolog Technology Reinforcement Learning Prover, Mining the Archive of Formal Proofs, Mizar: State-of-the-art and Beyond, \textsf{lazyCoP}: lazy paramodulation meets neurally guided search, Eliminating models during model elimination, Learning theorem proving components, System Description: E.T. 0.1, Aligning concepts across proof assistant libraries, A learning-based fact selector for Isabelle/HOL, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, The role of the Mizar mathematical library for interactive proof development in Mizar, VizAR: visualization of automated reasoning proofs (system description), 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, Encoding Monomorphic and Polymorphic Types, 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, Hierarchical invention of theorem proving strategies, Hammering Mizar by Learning Clause Guidance (Short Paper)., MaLeCoP Machine Learning Connection Prover, Theorem Proving in Large Formal Mathematics as an Emerging AI Field, Sledgehammer: Judgement Day, Extending Sledgehammer with SMT Solvers, Sine Qua Non for Large Theory Reasoning, Licensing the Mizar Mathematical Library, Extracting Higher-Order Goals from the Mizar Mathematical Library, ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\), MPTP 0.2, Semantics of Mizar as an Isabelle object logic, Presenting and Explaining Mizar, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\), Premise selection for mathematics by corpus analysis and kernel methods
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MPTP-motivation, implementation, first experiments
- 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
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- The TPTP problem library. CNF release v1. 2. 1
- On the rules of suppositions in formal logic
- On equivalents of well-foundedness. An experiment in MIZAR
- A Brief History of Natural Deduction
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Automated Deduction – CADE-19
