ATP and presentation service for Mizar formalizations (Q1945905): Difference between revisions

@@ Property / DOI @@
-.1007/s10817-012-9269-y
@@ Property / DOI: 10.1007/s10817-012-9269-y / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+Metis_
@@ Property / describes a project that uses: Metis_ / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MPTP 0.2
@@ Property / describes a project that uses: MPTP 0.2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MizarMode
@@ Property / describes a project that uses: MizarMode / 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 @@
+SystemOnTPTP
@@ Property / describes a project that uses: SystemOnTPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+kepler98
@@ Property / describes a project that uses: kepler98 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MML
@@ Property / describes a project that uses: MML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+seL4
@@ Property / describes a project that uses: seL4 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2399753239
@@ Property / OpenAlex ID: W2399753239 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.0616
@@ Property / arXiv ID: 1109.0616 / rank @@
+Normal rank
@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+A proof of the Kepler conjecture
@@ Property / cites work: A proof of the Kepler conjecture / rank @@
+Normal rank
@@ Property / cites work @@
+Sine Qua Non for Large Theory Reasoning
@@ Property / cites work: Sine Qua Non for Large Theory Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Lightweight relevance filtering for machine-generated resolution problems
+Normal rank
@@ Property / cites work @@
+Sur le coloriage des graphs
@@ Property / cites work: Sur le coloriage des graphs / rank @@
+Normal rank
@@ Property / cites work @@
+Simple Graphs as Simplicial Complexes: the Mycielskian of a Graph
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+Normal rank
@@ Property / cites work @@
+A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
+Normal rank
@@ Property / cites work @@
+Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
+Normal rank
@@ Property / cites work @@
+ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
+Normal rank
@@ Property / cites work @@
+MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
+Normal rank
@@ Property / cites work @@
+Automated Proof Compression by Invention of New Definitions
+Normal rank
@@ Property / DOI @@
+.1007/S10817-012-9269-Y
@@ Property / DOI: 10.1007/S10817-012-9269-Y / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:1945905