Learning Proof Transformations and Its Applications in Interactive Theorem Proving (Q6496633): Difference between revisions

@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+The role of the Mizar mathematical library for interactive proof development in Mizar
+Normal rank
@@ Property / cites work @@
+Mizar: State-of-the-art and Beyond
@@ Property / cites work: Mizar: State-of-the-art and Beyond / rank @@
+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 @@
+Internal Guidance for Satallax
@@ Property / cites work: Internal Guidance for Satallax / rank @@
+Normal rank
@@ Property / cites work @@
+Aligning concepts across proof assistant libraries
+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 @@
+SEPIA: Search for Proofs Using Inferred Automata
@@ Property / cites work: SEPIA: Search for Proofs Using Inferred Automata / rank @@
+Normal rank
@@ Property / cites work @@
+Q4619818
@@ Property / cites work: Q4619818 / rank @@
+Normal rank
@@ Property / cites work @@
+ENIGMA: efficient learning-based inference guiding machine
+Normal rank
@@ Property / cites work @@
+Automating formalization by statistical and semantic parsing of mathematics
+Normal rank
@@ Property / cites work @@
+Q4398828
@@ Property / cites work: Q4398828 / rank @@
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+Normal rank
@@ Property / cites work @@
+Q5219927
@@ Property / cites work: Q5219927 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5677085
@@ Property / cites work: Q5677085 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5624680
@@ Property / cites work: Q5624680 / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+Vampire with a brain is a good ITP hammer
@@ Property / cites work: Vampire with a brain is a good ITP hammer / rank @@
+Normal rank
@@ Property / cites work @@
+First neural conjecturing datasets and experiments
+Normal rank
@@ Property / cites work @@
+Online machine learning techniques for Coq: a comparison
+Normal rank