Hammering Mizar by Learning Clause Guidance (Short Paper). (Q5875448): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
(2 intermediate revisions by 2 users not shown) | |||
label / en | label / en | ||
Hammering Mizar by Learning Clause Guidance (Short Paper). | |||
Property / cites work | |||
Property / cites work: Premise selection for mathematics by corpus analysis and kernel methods / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A learning-based fact selector for Isabelle/HOL / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Hammering towards QED / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3096176 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Random Forests for Premise Selection / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Monte Carlo tableau proof search / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: TacticToe: Learning to Reason with HOL4 Tactics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: ENIGMAWatch: ProofWatch meets ENIGMA / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3075247 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: SEPIA: Search for Proofs Using Inferred Automata / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: ENIGMA: efficient learning-based inference guiding machine / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Enhancing ENIGMA given clause guidance / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: MizAR 40 for Mizar 40 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Lemmatization for Stronger Reasoning in Large Theories / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Deep Network Guided Proof Search / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3150301 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: System Description: E 1.8 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: MPTP 0.2: Design, implementation, and initial experiments / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: MaLeCoP Machine Learning Connection Prover / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2977777155 / rank | |||
Normal rank | |||
Property / title | |||
Hammering Mizar by Learning Clause Guidance (Short Paper). (English) | |||
Property / title: Hammering Mizar by Learning Clause Guidance (Short Paper). (English) / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 10:49, 31 July 2024
scientific article; zbMATH DE number 7649983
Language | Label | Description | Also known as |
---|---|---|---|
English | Hammering Mizar by Learning Clause Guidance (Short Paper). |
scientific article; zbMATH DE number 7649983 |
Statements
3 February 2023
0 references
proof automation
0 references
ITP hammers
0 references
automated theorem proving
0 references
machine learning
0 references
Hammering Mizar by Learning Clause Guidance (Short Paper). (English)
0 references