HOL Light: An Overview (Q3183517): Difference between revisions

@@ Property / describes a project that uses @@
+OCaml
@@ Property / describes a project that uses: OCaml / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Jordan
@@ Property / describes a project that uses: Jordan / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / 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-03359-9_4
+Normal rank
@@ Property / OpenAlex ID @@
+W1600435877
@@ Property / OpenAlex ID: W1600435877 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4726218
@@ Property / cites work: Q4726218 / rank @@
+Normal rank
@@ Property / cites work @@
+A formulation of the simple theory of types
@@ Property / cites work: A formulation of the simple theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+Axiom of Choice and Complementation
@@ Property / cites work: Axiom of Choice and Complementation / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+The Jordan Curve Theorem, Formally and Informally
@@ Property / cites work: The Jordan Curve Theorem, Formally and Informally / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Methods for Hardware Verification
@@ Property / cites work: Formal Methods for Hardware Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Nonlinear Real Formulas Via Sums of Squares
+Normal rank
@@ Property / cites work @@
+Formalizing an analytic proof of the prime number theorem
+Normal rank
@@ Property / cites work @@
+Q3727946
@@ Property / cites work: Q3727946 / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanical Theorem-Proving by Model Elimination
@@ Property / cites work: Mechanical Theorem-Proving by Model Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+A type-theoretical alternative to ISWIM, CUCH, OWHY
+Normal rank
@@ Property / cites work @@
+Some new results on decidability for elementary algebra and geometry
+Normal rank