\textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075): Difference between revisions

@@ 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 / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-030-86059-2_11
+Normal rank
@@ Property / OpenAlex ID @@
+W3196948051
@@ Property / OpenAlex ID: W3196948051 / rank @@
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
+Normal rank
@@ Property / cites work @@
+Internal Guidance for Satallax
@@ Property / cites work: Internal Guidance for Satallax / 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 @@
+TacticToe: learning to prove with tactics
@@ Property / cites work: TacticToe: learning to prove with tactics / rank @@
+Normal rank
@@ Property / cites work @@
+Layered clause selection for theory reasoning (short paper)
+Normal rank
@@ Property / cites work @@
+Make E Smart Again (Short Paper)
@@ Property / cites work: Make E Smart Again (Short Paper) / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
+Normal rank
@@ Property / cites work @@
+Controlled integration of the cut rule into connection tableau calculi
+Normal rank
@@ Property / cites work @@
+Q2751380
@@ Property / cites work: Q2751380 / 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 @@
+leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
+Normal rank
@@ Property / cites work @@
+Restricting backtracking in connection calculi
@@ Property / cites work: Restricting backtracking in connection calculi / rank @@
+Normal rank
@@ Property / cites work @@
+Connection tableaux with lazy paramodulation
@@ Property / cites work: Connection tableaux with lazy paramodulation / rank @@
+Normal rank
@@ Property / cites work @@
+A neurally-guided, parallel theorem prover
@@ Property / cites work: A neurally-guided, parallel theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Old or heavy? Decaying gracefully with age/weight shapes
+Normal rank
@@ Property / cites work @@
+Limited resource strategy in resolution theorem proving
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
+Normal rank
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
+Normal rank
@@ Property / cites work @@
+The CADE-14 ATP system competition
@@ Property / cites work: The CADE-14 ATP system competition / 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 @@
+Prolog Technology Reinforcement Learning Prover
@@ Property / cites work: Prolog Technology Reinforcement Learning Prover / rank @@
+Normal rank