Aligning concepts across proof assistant libraries (Q1640642): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / 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 @@
+MoMM
@@ Property / describes a project that uses: MoMM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Polar
@@ Property / describes a project that uses: Polar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Matita
@@ Property / describes a project that uses: Matita / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CoqHammer
@@ Property / describes a project that uses: CoqHammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lean
@@ Property / describes a project that uses: Lean / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / 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 / describes a project that uses @@
+ileanCoP
@@ Property / describes a project that uses: ileanCoP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OpenTheory
@@ Property / describes a project that uses: OpenTheory / 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.2018.04.005
+Normal rank
@@ Property / OpenAlex ID @@
+W2810678140
@@ Property / OpenAlex ID: W2810678140 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q108482111
@@ Property / Wikidata QID: Q108482111 / rank @@
+Normal rank
@@ Property / cites work @@
+Matita Tutorial
@@ Property / cites work: Matita Tutorial / rank @@
+Normal rank
@@ Property / cites work @@
+What’s in a Theorem Name?
@@ Property / cites work: What’s in a Theorem Name? / rank @@
+Normal rank
@@ Property / cites work @@
+Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
+Normal rank
@@ Property / cites work @@
+Markov Chains and Dynamical Systems: The Open System Point of View
+Normal rank
@@ Property / cites work @@
+Category Theory
@@ Property / cites work: Category Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Mizar: State-of-the-art and Beyond
@@ Property / cites work: Mizar: State-of-the-art and Beyond / rank @@
+Normal rank
@@ Property / cites work @@
+A learning-based fact selector for Isabelle/HOL
@@ Property / cites work: A learning-based fact selector for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Q4447247
@@ Property / cites work: Q4447247 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3431400
@@ Property / cites work: Q3431400 / rank @@
+Normal rank
@@ Property / cites work @@
+Cooperative Repositories for Formal Proofs
@@ Property / cites work: Cooperative Repositories for Formal Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Hammer for Coq: automation for dependent type theory
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+Normal rank
@@ Property / cites work @@
+Polar: A Framework for Proof Refactoring
@@ Property / cites work: Polar: A Framework for Proof Refactoring / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem proving modulo
@@ Property / cites work: Theorem proving modulo / 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 @@
+Sharing HOL4 and HOL Light Proof Knowledge
@@ Property / cites work: Sharing HOL4 and HOL Light Proof Knowledge / rank @@
+Normal rank
@@ Property / cites work @@
+Four decades of {\textsc{Mizar}}. Foreword
@@ Property / cites work: Four decades of {\textsc{Mizar}}. Foreword / rank @@
+Normal rank
@@ Property / cites work @@
+Data Refinement in Isabelle/HOL
@@ Property / cites work: Data Refinement in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Light: An Overview
@@ Property / cites work: HOL Light: An Overview / rank @@
+Normal rank
@@ Property / cites work @@
+The HOL Light theory of Euclidean space
@@ Property / cites work: The HOL Light theory of Euclidean space / rank @@
+Normal rank
@@ Property / cites work @@
+Q4619818
@@ Property / cites work: Q4619818 / rank @@
+Normal rank
@@ Property / cites work @@
+Recycling proof patterns in Coq: case studies
@@ Property / cites work: Recycling proof patterns in Coq: case studies / rank @@
+Normal rank
@@ Property / cites work @@
+Stability and convergence in strongly monotone dynamical systems.
+Normal rank
@@ Property / cites work @@
+years of research and development around Coq
@@ Property / cites work: 30 years of research and development around Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Scalable LCF-Style Proof Translation
@@ Property / cites work: Scalable LCF-Style Proof Translation / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+HOL(y)Hammer: online ATP service for HOL Light
@@ Property / cites work: HOL(y)Hammer: online ATP service for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted theorem proving with millions of lemmas
+Normal rank
@@ Property / cites work @@
+Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
+Normal rank
@@ Property / cites work @@
+Importing HOL Light into Coq
@@ Property / cites work: Importing HOL Light into Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Classification of alignments between concepts of formal mathematical systems
+Normal rank
@@ Property / cites work @@
+The Reflective Milawa Theorem Prover Is Sound
@@ Property / cites work: The Reflective Milawa Theorem Prover Is Sound / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning with Analytic Tableaux and Related Methods
+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 @@
+Q2751378
@@ Property / cites work: Q2751378 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3407081
@@ Property / cites work: Q3407081 / rank @@
+Normal rank
@@ Property / cites work @@
+Simple and Efficient Clause Subsumption with Feature Vector Indexing
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP Typed First-Order Form with Arithmetic
@@ Property / cites work: The TPTP Typed First-Order Form with Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+Normal rank
@@ Property / cites work @@
+Automata, languages and programming. 25th international colloquium, ICALP '98. Aalborg, Denmark, July 13--17, 1998. Proceedings
+Normal rank
@@ Property / cites work @@
+The Isabelle Framework
@@ Property / cites work: The Isabelle Framework / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Formal Proof Script Refactoring
@@ Property / cites work: Towards Formal Proof Script Refactoring / rank @@
+Normal rank