Mizar: State-of-the-art and Beyond (Q3453119): Difference between revisions

@@ Property / describes a project that uses @@
+MaLeCoP
@@ Property / describes a project that uses: MaLeCoP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MaLARea
@@ Property / describes a project that uses: MaLARea / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MPTP
@@ Property / describes a project that uses: MPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MML
@@ Property / describes a project that uses: MML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+BliStr
@@ Property / describes a project that uses: BliStr / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+miz3
@@ Property / describes a project that uses: miz3 / 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-319-20615-8_17
+Normal rank
@@ Property / OpenAlex ID @@
+W2295728669
@@ Property / OpenAlex ID: W2295728669 / rank @@
+Normal rank
@@ Property / cites work @@
+mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
+Normal rank
@@ Property / cites work @@
+Eliciting implicit assumptions of Mizar proofs by property omission
+Normal rank
@@ Property / cites work @@
+Large Formal Wikis: Issues and Solutions
@@ Property / cites work: Large Formal Wikis: Issues and Solutions / rank @@
+Normal rank
@@ Property / cites work @@
+Licensing the Mizar Mathematical Library
@@ Property / cites work: Licensing the Mizar Mathematical Library / rank @@
+Normal rank
@@ Property / cites work @@
+Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Information Retrieval and Rendering with MML Query
+Normal rank
@@ Property / cites work @@
+A compendium of continuous lattices in MIZAR
@@ Property / cites work: A compendium of continuous lattices in MIZAR / rank @@
+Normal rank
@@ Property / cites work @@
+Q4413887
@@ Property / cites work: Q4413887 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+New Developments in Parsing Mizar
@@ Property / cites work: New Developments in Parsing Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+A Declarative Language for the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+A Symbolic Companion for Interactive Geometric Systems
+Normal rank
@@ Property / cites work @@
+Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar
+Normal rank
@@ Property / cites work @@
+Efficient Rough Set Theory Merging
@@ Property / cites work: Efficient Rough Set Theory Merging / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Revisions as an Essential Tool to Maintain Mathematical Repositories
+Normal rank
@@ Property / cites work @@
+The Mizar Mathematical Library in OMDoc: translation and applications
+Normal rank
@@ Property / cites work @@
+MizAR 40 for Mizar 40
@@ Property / cites work: MizAR 40 for Mizar 40 / rank @@
+Normal rank
@@ Property / cites work @@
+On rewriting rules in Mizar
@@ Property / cites work: On rewriting rules in Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+An example of formalizing recent mathematical results in MIZAR
+Normal rank
@@ Property / cites work @@
+Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking
+Normal rank
@@ Property / cites work @@
+SAT-Enhanced Mizar Proof Checking
@@ Property / cites work: SAT-Enhanced Mizar Proof Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of Mizar
@@ Property / cites work: A Brief Overview of Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+Methods of lemma extraction in natural deduction proofs
+Normal rank
@@ Property / cites work @@
+Improving legibility of natural deduction proofs is not trivial
+Normal rank
@@ Property / cites work @@
+Q4413892
@@ Property / cites work: Q4413892 / rank @@
+Normal rank
@@ Property / cites work @@
+MPTP-motivation, implementation, first experiments
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+Normal rank
@@ Property / cites work @@
+A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+Normal rank
@@ Property / cites work @@
+ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
+Normal rank
@@ Property / cites work @@
+MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
+Normal rank
@@ Property / cites work @@
+MaLeCoP Machine Learning Connection Prover
@@ Property / cites work: MaLeCoP Machine Learning Connection Prover / rank @@
+Normal rank
@@ Property / cites work @@
+A comparison of Mizar and Isar
@@ Property / cites work: A comparison of Mizar and Isar / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790672
@@ Property / cites work: Q4790672 / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q5302561
@@ Property / cites work: Q5302561 / rank @@
+Normal rank
@@ Property / cites work @@
+A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
+Normal rank