Lemmatization for Stronger Reasoning in Large Theories
From MaRDI portal
Publication:2964472
DOI10.1007/978-3-319-24246-0_21zbMath1471.68313OpenAlexW2295529234WikidataQ108482155 ScholiaQ108482155MaRDI QIDQ2964472
Josef Urban, Cezary Kaliszyk, Jiří Vyskočil
Publication date: 27 February 2017
Published in: Frontiers of Combining Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-24246-0_21
Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (4)
MizAR 40 for Mizar 40 ⋮ System Description: E.T. 0.1 ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper).
Uses Software
Cites Work
- MizAR 40 for Mizar 40
- Learning-assisted theorem proving with millions of lemmas
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- System Description: E 1.8
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- Automated theorem proving in quasigroup and loop theory
- SRASS - A Semantic Relevance Axiom Selection System
- Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction
- MaSh: Machine Learning for Sledgehammer
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Lemmatization for Stronger Reasoning in Large Theories
