Vampire with a brain is a good ITP hammer (Q831938): Difference between revisions

@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Hammering towards QED
@@ Property / cites work: Hammering towards QED / rank @@
+Normal rank
@@ Property / cites work @@
+ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
+Normal rank
@@ Property / cites work @@
+Learning domain knowledge to improve theorem proving
+Normal rank
@@ Property / cites work @@
+Random Forests for Premise Selection
@@ Property / cites work: Random Forests for Premise Selection / rank @@
+Normal rank
@@ Property / cites work @@
+Monte Carlo tableau proof search
@@ Property / cites work: Monte Carlo tableau proof search / rank @@
+Normal rank
@@ Property / cites work @@
+Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
+Normal rank
@@ Property / cites work @@
+Layered clause selection for theory reasoning (short paper)
+Normal rank
@@ Property / cites work @@
+Q5270493
@@ Property / cites work: Q5270493 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+Sine Qua Non for Large Theory Reasoning
@@ Property / cites work: Sine Qua Non for Large Theory Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
+Normal rank
@@ Property / cites work @@
+ENIGMA: efficient learning-based inference guiding machine
+Normal rank
@@ Property / cites work @@
+Enhancing ENIGMA given clause guidance
@@ Property / cites work: Enhancing ENIGMA given clause guidance / rank @@
+Normal rank
@@ Property / cites work @@
+Hammering Mizar by Learning Clause Guidance (Short Paper).
+Normal rank
@@ Property / cites work @@
+MizAR 40 for Mizar 40
@@ Property / cites work: MizAR 40 for Mizar 40 / rank @@
+Normal rank
@@ Property / cites work @@
+Deep Network Guided Proof Search
@@ Property / cites work: Deep Network Guided Proof Search / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751359
@@ Property / cites work: Q2751359 / rank @@
+Normal rank
@@ Property / cites work @@
+Playing with AVATAR
@@ Property / cites work: Playing with AVATAR / rank @@
+Normal rank
@@ Property / cites work @@
+Limited resource strategy in resolution theorem proving
+Normal rank
@@ Property / cites work @@
+Q5290112
@@ Property / cites work: Q5290112 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2739546
@@ Property / cites work: Q2739546 / rank @@
+Normal rank
@@ Property / cites work @@
+Faster, higher, stronger: E 2.3
@@ Property / cites work: Faster, higher, stronger: E 2.3 / rank @@
+Normal rank
@@ Property / cites work @@
+Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
+Normal rank
@@ Property / cites work @@
+Q2934059
@@ Property / cites work: Q2934059 / rank @@
+Normal rank
@@ Property / cites work @@
+Improving ENIGMA-style clause selection while learning from history
+Normal rank
@@ Property / cites work @@
+GKC: a reasoning system for large knowledge bases
@@ Property / cites work: GKC: a reasoning system for large knowledge bases / rank @@
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+Normal rank
@@ Property / cites work @@
+MaLeCoP Machine Learning Connection Prover
@@ Property / cites work: MaLeCoP Machine Learning Connection Prover / rank @@
+Normal rank
@@ Property / cites work @@
+AVATAR: The Architecture for First-Order Theorem Provers
+Normal rank