The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215): Difference between revisions

@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+seL4
@@ Property / describes a project that uses: seL4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+DeepMath
@@ Property / describes a project that uses: DeepMath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Logic2CNF
@@ Property / describes a project that uses: Logic2CNF / 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/s10817-017-9440-6
+Normal rank
@@ Property / OpenAlex ID @@
+W2770430340
@@ Property / OpenAlex ID: W2770430340 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+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 @@
+mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
+Normal rank
@@ Property / cites work @@
+Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19--21, 2004. Proceedings.
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+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 @@
+MPTP 0.2: Design, implementation, and initial experiments
+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 @@
+Mining the Archive of Formal Proofs
@@ Property / cites work: Mining the Archive of Formal Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Hammering towards QED
@@ Property / cites work: Hammering towards QED / rank @@
+Normal rank
@@ Property / cites work @@
+Mizar Course in Logic and Set Theory
@@ Property / cites work: Mizar Course in Logic and Set Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q5590633
@@ Property / cites work: Q5590633 / rank @@
+Normal rank
@@ Property / cites work @@
+Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings
+Normal rank
@@ Property / cites work @@
+Q5610115
@@ Property / cites work: Q5610115 / rank @@
+Normal rank
@@ Property / cites work @@
+Aligning concepts across proof assistant libraries
+Normal rank
@@ Property / cites work @@
+Q3898534
@@ Property / cites work: Q3898534 / rank @@
+Normal rank
@@ Property / cites work @@
+Continuous Lattices and Domains
@@ Property / cites work: Continuous Lattices and Domains / 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 @@
+Methods of lemma extraction in natural deduction proofs
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
+Normal rank
@@ Property / cites work @@
+Revisions as an Essential Tool to Maintain Mathematical Repositories
+Normal rank
@@ Property / cites work @@
+Mechanizing complemented lattices within Mizar type system
+Normal rank
@@ Property / cites work @@
+Lattice Theory for Rough Sets – A Case Study with Mizar
+Normal rank
@@ Property / cites work @@
+Q3075247
@@ Property / cites work: Q3075247 / 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 @@
+A FORMAL PROOF OF THE KEPLER CONJECTURE
@@ Property / cites work: A FORMAL PROOF OF THE KEPLER CONJECTURE / rank @@
+Normal rank
@@ Property / cites work @@
+The Mizar Mathematical Library in OMDoc: translation and applications
+Normal rank
@@ Property / cites work @@
+System Description: E.T. 0.1
@@ Property / cites work: System Description: E.T. 0.1 / rank @@
+Normal rank
@@ Property / cites work @@
+Glushkov's evidence algorithm
@@ Property / cites work: Glushkov's evidence algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+Lemmatization for Stronger Reasoning in Large Theories
+Normal rank
@@ Property / cites work @@
+Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
+Normal rank
@@ Property / cites work @@
+Learning-assisted theorem proving with millions of lemmas
+Normal rank
@@ Property / cites work @@
+MizAR 40 for Mizar 40
@@ Property / cites work: MizAR 40 for Mizar 40 / rank @@
+Normal rank
@@ Property / cites work @@
+Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings
+Normal rank
@@ Property / cites work @@
+Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25--29, 2016. Proceedings
+Normal rank
@@ Property / cites work @@
+Enhancement of Mizar Texts with Transitivity Property of Predicates
+Normal rank
@@ Property / cites work @@
+On rewriting rules in Mizar
@@ Property / cites work: On rewriting rules in Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+Flexary connectives in Mizar
@@ Property / cites work: Flexary connectives in Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+Deep Network Guided Proof Search
@@ Property / cites work: Deep Network Guided Proof Search / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Accessing the Mizar Library with a Weakly Strict Mizar Parser
+Normal rank
@@ Property / cites work @@
+SAT-Enhanced Mizar Proof Checking
@@ Property / cites work: SAT-Enhanced Mizar Proof Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Tools for MML Environment Analysis
@@ Property / cites work: Tools for MML Environment Analysis / rank @@
+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 @@
+Automated Improving of Proof Legibility in the Mizar System
+Normal rank
@@ Property / cites work @@
+Improving legibility of formal proofs based on the close reference principle is NP-hard
+Normal rank
@@ Property / cites work @@
+Q2767928
@@ Property / cites work: Q2767928 / rank @@
+Normal rank
@@ Property / cites work @@
+The 8th IJCAR automated theorem proving system competition – CASC-J8
+Normal rank
@@ Property / cites work @@
+On well-ordered subsets of any set
@@ Property / cites work: On well-ordered subsets of any set / rank @@
+Normal rank
@@ Property / cites work @@
+On Better-Quasi-Ordering Countable Series-Parallel Orders
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+MPTP-motivation, implementation, first experiments
+Normal rank
@@ Property / cites work @@
+ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
+Normal rank
@@ Property / cites work @@
+Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
+Normal rank