Lemmatization for stronger reasoning in large theories
DOI10.1007/978-3-319-24246-0_21zbMATH Open1471.68313OpenAlexW2295529234WikidataQ108482155 ScholiaQ108482155MaRDI QIDQ2964472FDOQ2964472
Authors: Cezary Kaliszyk, Josef Urban, 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
Recommendations
Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- MizAR 40 for Mizar 40
- System description: E 1.8
- Title not available (Why is that?)
- SRASS - A Semantic Relevance Axiom Selection System
- Title not available (Why is that?)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- MaSh: machine learning for Sledgehammer
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Learning search control-knowledge for equational deduction
- Learning-assisted theorem proving with millions of lemmas
- Loops with abelian inner mapping groups: an application of automated deduction
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Automated theorem proving in quasigroup and loop theory
Cited In (14)
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- On the generation of quantified lemmas
- Formalising the Kruskal-Katona theorem in Lean
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Title not available (Why is that?)
- The role of the Mizar mathematical library for interactive proof development in Mizar
- MizAR 40 for Mizar 40
- System description: E.T. 0.1
- An abstraction-refinement framework for reasoning with large theories
- Learning-assisted theorem proving with millions of lemmas
- Voting theory in the Lean theorem prover
- Lemmas: generation, selection, application
- ATPboost: learning premise selection in binary setting with ATP feedback
- Large theory reasoning with SUMO at CASC
Uses Software
This page was built for publication: Lemmatization for stronger reasoning in large theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2964472)
