Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871): Difference between revisions

@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MiniSat
@@ Property / describes a project that uses: MiniSat / 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 @@
+LEO-II
@@ Property / describes a project that uses: LEO-II / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OTTER
@@ Property / describes a project that uses: OTTER / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPASS
@@ Property / describes a project that uses: SPASS / 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 @@
+MaLeCoP
@@ Property / describes a project that uses: MaLeCoP / 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 @@
+MaLARea
@@ Property / describes a project that uses: MaLARea / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2155552045
@@ Property / OpenAlex ID: W2155552045 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.3914
@@ Property / arXiv ID: 1209.3914 / rank @@
+Normal rank
@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+Automated and Human Proofs in General Mathematics: An Initial Comparison
+Normal rank
@@ Property / cites work @@
+Superposition Modulo Linear Arithmetic SUP(LA)
@@ Property / cites work: Superposition Modulo Linear Arithmetic SUP(LA) / rank @@
+Normal rank
@@ Property / cites work @@
+LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+On deciding satisfiability by theorem proving with speculative inferences
+Normal rank
@@ Property / cites work @@
+Satallax: An Automatic Higher-Order Prover
@@ Property / cites work: Satallax: An Automatic Higher-Order Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+On the rules of suppositions in formal logic
@@ Property / cites work: On the rules of suppositions in formal logic / rank @@
+Normal rank
@@ Property / cites work @@
+Integrating Linear Arithmetic into Superposition Calculus
+Normal rank
@@ Property / cites work @@
+Lightweight relevance filtering for machine-generated resolution problems
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q2751358
@@ Property / cites work: Q2751358 / 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 @@
+Automated deduction in von Neumann-Bernays-Gödel set theory
+Normal rank
@@ Property / cites work @@
+Q4032144
@@ Property / cites work: Q4032144 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150300
@@ Property / cites work: Q3150300 / rank @@
+Normal rank
@@ Property / cites work @@
+SRASS - A Semantic Relevance Axiom Selection System
+Normal rank
@@ Property / cites work @@
+The TPTP World – Infrastructure for Automated Reasoning
+Normal rank
@@ Property / cites work @@
+Q4413895
@@ Property / cites work: Q4413895 / rank @@
+Normal rank
@@ Property / cites work @@
+MPTP-motivation, implementation, first experiments
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+Normal rank
@@ Property / cites work @@
+ATP Cross-Verification of the Mizar MPTP Challenge Problems
+Normal rank
@@ Property / cites work @@
+A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+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