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

@@ Property / describes a project that uses @@
+ENIGMA
@@ Property / describes a project that uses: ENIGMA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+XGBoost
@@ Property / describes a project that uses: XGBoost / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOList
@@ Property / describes a project that uses: HOList / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Tactician
@@ Property / describes a project that uses: Tactician / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TacticToe
@@ Property / describes a project that uses: TacticToe / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ATPboost
@@ Property / describes a project that uses: ATPboost / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3186870373
@@ Property / OpenAlex ID: W3186870373 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.05207
@@ Property / arXiv ID: 2104.05207 / rank @@
+Normal rank
@@ 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