Online machine learning techniques for Coq: a comparison (Q2128797): Difference between revisions

@@ Property / cites work @@
+Multidimensional binary search trees used for associative searching
+Normal rank
@@ Property / cites work @@
+The Tactician. A seamless, interactive tactic learner and prover for Coq
+Normal rank
@@ Property / cites work @@
+Random forests
@@ Property / cites work: Random forests / rank @@
+Normal rank
@@ Property / cites work @@
+ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
+Normal rank
@@ Property / cites work @@
+Making data structures persistent
@@ Property / cites work: Making data structures persistent / rank @@
+Normal rank
@@ Property / cites work @@
+Random Forests for Premise Selection
@@ Property / cites work: Random Forests for Premise Selection / rank @@
+Normal rank
@@ Property / cites work @@
+TacticToe: Learning to Reason with HOL4 Tactics
@@ Property / cites work: TacticToe: Learning to Reason with HOL4 Tactics / rank @@
+Normal rank
@@ Property / cites work @@
+TacticToe: learning to prove with tactics
@@ Property / cites work: TacticToe: learning to prove with tactics / rank @@
+Normal rank
@@ Property / cites work @@
+Q2913814
@@ Property / cites work: Q2913814 / rank @@
+Normal rank
@@ Property / cites work @@
+A proof strategy language and proof script generation for Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+ATPboost: learning premise selection in binary setting with ATP feedback
+Normal rank