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

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Learning-assisted theorem proving with millions of lemmas
• scientific article; zbMATH DE number 1612567
• Lemma Mining over HOL Light
• The use of lemmas in the model elimination procedure
• On terminating lemma speculations.

Cites work

• scientific article; zbMATH DE number 1614717 (Why is no real title available?)
• scientific article; zbMATH DE number 1765686 (Why is no real title available?)
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• Automated theorem proving in quasigroup and loop theory
• Learning search control-knowledge for equational deduction
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Learning-assisted theorem proving with millions of lemmas
• Loops with abelian inner mapping groups: an application of automated deduction
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• MaSh: machine learning for Sledgehammer
• MizAR 40 for Mizar 40
• Premise selection for mathematics by corpus analysis and kernel methods
• SRASS - A Semantic Relevance Axiom Selection System
• System description: E 1.8
• Using hints to increase the effectiveness of an automated reasoning program: Case studies

Cited in

(14)

• Formalising the Kruskal-Katona theorem in Lean
• scientific article; zbMATH DE number 1612567 (Why is no real title available?)
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• MizAR 40 for Mizar 40
• System description: E.T. 0.1
• On the generation of quantified lemmas
• Lemmas: generation, selection, application
• Deep Generation of Coq Lemma Names Using Elaborated Terms
• Voting theory in the Lean theorem prover
• Large theory reasoning with SUMO at CASC
• An abstraction-refinement framework for reasoning with large theories
• Learning-assisted theorem proving with millions of lemmas
• ATPboost: learning premise selection in binary setting with ATP feedback

Describes a project that uses

Uses Software

• VAMPIRE
• MoMM
• MaSh
• Flyspeck
• MaLARea
• BliStr
• TRAMP
• P.rex
• SRASS

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)