Composable Discovery Engines for Interactive Theorem Proving (Q3088022): Difference between revisions

@@ Property / author @@
-Jacques D. Fleuriot
@@ Property / author: Jacques D. Fleuriot / rank @@
-Normal rank
@@ Property / author @@
+Jacques D. Fleuriot
@@ Property / author: Jacques D. Fleuriot / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / 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-642-22863-6_28
+Normal rank
@@ Property / OpenAlex ID @@
+W2139827631
@@ Property / OpenAlex ID: W2139827631 / rank @@
+Normal rank
@@ Property / cites work @@
+Applicative programming with effects
@@ Property / cites work: Applicative programming with effects / rank @@
+Normal rank
@@ Property / cites work @@
+Automation for interactive proof: first prototype
@@ Property / cites work: Automation for interactive proof: first prototype / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous
+Normal rank
@@ Property / cites work @@
+Algebras for combinatorial search
@@ Property / cites work: Algebras for combinatorial search / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790672
@@ Property / cites work: Q4790672 / rank @@
+Normal rank