A verified common lisp implementation of Buchberger's algorithm in ACL2 (Q1034553): Difference between revisions

@@ Property / author @@
+José Luis Ruiz-Reina
@@ Property / author: José Luis Ruiz-Reina / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Theorema
@@ Property / describes a project that uses: Theorema / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+NQTHM
@@ Property / describes a project that uses: NQTHM / 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 @@
+LISP
@@ Property / describes a project that uses: LISP / 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.1016/j.jsc.2009.07.002
+Normal rank
@@ Property / OpenAlex ID @@
+W2004470082
@@ Property / OpenAlex ID: W2004470082 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q57834883
@@ Property / Wikidata QID: Q57834883 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4040283
@@ Property / cites work: Q4040283 / rank @@
+Normal rank
@@ Property / cites work @@
+Ein algorithmisches Kriterium für die Lösbarkeit eines algebraischen Gleichungssystems
+Normal rank
@@ Property / cites work @@
+Q3021905
@@ Property / cites work: Q3021905 / rank @@
+Normal rank
@@ Property / cites work @@
+Bruno Buchberger's PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Translation from the German
+Normal rank
@@ Property / cites work @@
+Q3416408
@@ Property / cites work: Q3416408 / rank @@
+Normal rank
@@ Property / cites work @@
+\textit{Theorema}: Towards computer-aided mathematical theory exploration
+Normal rank
@@ Property / cites work @@
+Q4377762
@@ Property / cites work: Q4377762 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4944848
@@ Property / cites work: Q4944848 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4023676
@@ Property / cites work: Q4023676 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient execution in an automated reasoning environment
+Normal rank
@@ Property / cites work @@
+Certifying properties of an efficient functional program for computing Gröbner bases
+Normal rank
@@ Property / cites work @@
+Structured theory development for a mechanized logic
+Normal rank
@@ Property / cites work @@
+Q3408130
@@ Property / cites work: Q3408130 / rank @@
+Normal rank
@@ Property / cites work @@
+Commutative algebra in the Mizar system
@@ Property / cites work: Commutative algebra in the Mizar system / rank @@
+Normal rank
@@ Property / cites work @@
+Formal proofs about rewriting using ACL2
@@ Property / cites work: Formal proofs about rewriting using ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Q3997095
@@ Property / cites work: Q3997095 / rank @@
+Normal rank
@@ Property / cites work @@
+A machine-checked implementation of Buchberger's algorithm
+Normal rank