The role of entropy in guiding a connection prover (Q2142077): Difference between revisions

@@ Property / describes a project that uses @@
+FEMaLeCoP
@@ Property / describes a project that uses: FEMaLeCoP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / 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 @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+DeepMath
@@ Property / describes a project that uses: DeepMath / 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 @@
+ENIGMA
@@ Property / describes a project that uses: ENIGMA / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3201967611
@@ Property / OpenAlex ID: W3201967611 / rank @@
+Normal rank
@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+A vision for automated deduction rooted in the connection method
+Normal rank
@@ Property / cites work @@
+The Tactician. A seamless, interactive tactic learner and prover for Coq
+Normal rank
@@ Property / cites work @@
+ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
+Normal rank
@@ Property / cites work @@
+Q4457464
@@ Property / cites work: Q4457464 / rank @@
+Normal rank
@@ Property / cites work @@
+Machine learning guidance for connection tableaux
@@ Property / cites work: Machine learning guidance for connection tableaux / 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 @@
+Q5287513
@@ Property / cites work: Q5287513 / 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 @@
+FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
+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 @@
+Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
+Normal rank
@@ Property / cites work @@
+Q4999300
@@ Property / cites work: Q4999300 / rank @@
+Normal rank
@@ Property / cites work @@
+leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
+Normal rank
@@ Property / cites work @@
+IeanCOP: lean connection-based theorem proving
@@ Property / cites work: IeanCOP: lean connection-based theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: E 1.8
@@ Property / cites work: System Description: E 1.8 / 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 @@
+Q4626283
@@ Property / cites work: Q4626283 / rank @@
+Normal rank
@@ Property / cites work @@
+MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
+Normal rank
@@ Property / cites work @@
+MaLeCoP Machine Learning Connection Prover
@@ Property / cites work: MaLeCoP Machine Learning Connection Prover / rank @@
+Normal rank
@@ Property / cites work @@
+The Isabelle Framework
@@ Property / cites work: The Isabelle Framework / rank @@
+Normal rank
@@ Property / cites work @@
+Prolog Technology Reinforcement Learning Prover
@@ Property / cites work: Prolog Technology Reinforcement Learning Prover / rank @@
+Normal rank