Towards finding longer proofs (Q2142073): Difference between revisions

@@ Property / cites work @@
+Term Rewriting and All That
@@ Property / cites work: Term Rewriting and All That / rank @@
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q3817655
@@ Property / cites work: Q3817655 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3804239
@@ Property / cites work: Q3804239 / rank @@
+Normal rank
@@ Property / cites work @@
+ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
+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 @@
+A shortest single axiom for the classical equivalential calculus
+Normal rank
@@ Property / cites work @@
+Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction
+Normal rank
@@ Property / cites work @@
+Deep Network Guided Proof Search
@@ Property / cites work: Deep Network Guided Proof Search / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264737
@@ Property / cites work: Q4264737 / rank @@
+Normal rank
@@ Property / cites work @@
+Knowledge-based proof planning
@@ Property / cites work: Knowledge-based proof planning / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q4999300
@@ Property / cites work: Q4999300 / rank @@
+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 @@
+Shortest single axioms for the classical equivalential calculus
+Normal rank
@@ Property / cites work @@
+Guiding inferences in connection tableau by recurrent neural networks
+Normal rank
@@ Property / cites work @@
+Q5828994
@@ Property / cites work: Q5828994 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5839903
@@ Property / cites work: Q5839903 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2724150
@@ Property / cites work: Q2724150 / 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 @@
+The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
+Normal rank
@@ Property / cites work @@
+Q4626283
@@ Property / cites work: Q4626283 / rank @@
+Normal rank
@@ Property / cites work @@
+First neural conjecturing datasets and experiments
+Normal rank
@@ Property / cites work @@
+MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
+Normal rank
@@ Property / cites work @@
+Using hints to increase the effectiveness of an automated reasoning program: Case studies
+Normal rank
@@ Property / cites work @@
+A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
+Normal rank
@@ Property / cites work @@
+Meeting the challenge of fifty years of logic
@@ Property / cites work: Meeting the challenge of fifty years of logic / rank @@
+Normal rank
@@ Property / cites work @@
+Prolog Technology Reinforcement Learning Prover
@@ Property / cites work: Prolog Technology Reinforcement Learning Prover / 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 @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+lazyCoP
@@ Property / describes a project that uses: lazyCoP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ENIGMA
@@ Property / describes a project that uses: ENIGMA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VAMPIRE
@@ Property / describes a project that uses: VAMPIRE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+E Theorem Prover
@@ Property / describes a project that uses: E Theorem Prover / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OpenAI Gym
@@ Property / describes a project that uses: OpenAI Gym / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TPTP
@@ Property / describes a project that uses: TPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Stable Baselines
@@ Property / describes a project that uses: Stable Baselines / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MaLARea
@@ Property / describes a project that uses: MaLARea / rank @@
+Normal rank
@@ 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 / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3202968181
@@ Property / OpenAlex ID: W3202968181 / rank @@
+Normal rank