Towards Knowledge Management for HOL Light (Q5495935): Difference between revisions

@@ Property / cites work @@
+Cooperative Repositories for Formal Proofs
@@ Property / cites work: Cooperative Repositories for Formal Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+IMPS: An interactive mathematical proof system
@@ Property / cites work: IMPS: An interactive mathematical proof system / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Matching Concepts across HOL Libraries
@@ Property / cites work: Matching Concepts across HOL Libraries / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Extending MKM Formats at the Statement Level
@@ Property / cites work: Extending MKM Formats at the Statement Level / rank @@
+Normal rank
@@ Property / cites work @@
+Flexary Operators for Formalized Mathematics
@@ Property / cites work: Flexary Operators for Formalized Mathematics / rank @@
+Normal rank
@@ Property / cites work @@
+The Mizar Mathematical Library in OMDoc: translation and applications
+Normal rank
@@ Property / cites work @@
+Scalable LCF-Style Proof Translation
@@ Property / cites work: Scalable LCF-Style Proof Translation / rank @@
+Normal rank
@@ Property / cites work @@
+A Search Engine for Mathematical Formulae
@@ Property / cites work: A Search Engine for Mathematical Formulae / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+Importing HOL Light into Coq
@@ Property / cites work: Importing HOL Light into Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790669
@@ Property / cites work: Q4790669 / rank @@
+Normal rank
@@ Property / cites work @@
+Capturing Hiproofs in HOL Light
@@ Property / cites work: Capturing Hiproofs in HOL Light / 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 @@
+The MMT API: A Generic MKM System
@@ Property / cites work: The MMT API: A Generic MKM System / rank @@
+Normal rank
@@ Property / cites work @@
+A scalable module system
@@ Property / cites work: A scalable module system / rank @@
+Normal rank
@@ Property / cites work @@
+A Foundational View on Integration Problems
@@ Property / cites work: A Foundational View on Integration Problems / rank @@
+Normal rank
@@ Property / cites work @@
+Proviola: A Tool for Proof Re-animation
@@ Property / cites work: Proviola: A Tool for Proof Re-animation / rank @@
+Normal rank
@@ Property / cites work @@
+Communicating Formal Proofs: The Case of Flyspeck
@@ Property / cites work: Communicating Formal Proofs: The Case of Flyspeck / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Mathematics on Display: A Wiki for Flyspeck
+Normal rank