Semantics of Mizar as an Isabelle object logic (Q2323445): Difference between revisions

@@ Property / DOI @@
-.1007/s10817-018-9479-z
@@ Property / DOI: 10.1007/s10817-018-9479-z / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/PIDE
@@ Property / describes a project that uses: Isabelle/PIDE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ProofPeer
@@ Property / describes a project that uses: ProofPeer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Rodin
@@ Property / describes a project that uses: Rodin / 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 @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/Isar
@@ Property / describes a project that uses: Isabelle/Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPASS
@@ Property / describes a project that uses: SPASS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/ZF
@@ Property / describes a project that uses: Isabelle/ZF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OMDoc
@@ Property / describes a project that uses: OMDoc / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nitpick
@@ Property / describes a project that uses: Nitpick / 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 @@
+miz3
@@ Property / describes a project that uses: miz3 / 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-018-9479-z
+Normal rank
@@ Property / OpenAlex ID @@
+W2889093133
@@ Property / OpenAlex ID: W2889093133 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q108482110
@@ Property / Wikidata QID: Q108482110 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3569584
@@ Property / cites work: Q3569584 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Auditing Formalised Mathematics
@@ Property / cites work: Proof Auditing Formalised Mathematics / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024857
@@ Property / cites work: Q3024857 / rank @@
+Normal rank
@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+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 @@
+The role of the Mizar mathematical library for interactive proof development in Mizar
+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 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 @@
+Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface
+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 @@
+Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
+Normal rank
@@ Property / cites work @@
+Extracting Higher-Order Goals from the Mizar Mathematical Library
+Normal rank
@@ Property / cites work @@
+A Declarative Language for the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+Q4503907
@@ Property / cites work: Q4503907 / rank @@
+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 @@
+Random-Access Stored-Program Machines, an Approach to Programming Languages
+Normal rank
@@ Property / cites work @@
+Q5815602
@@ Property / cites work: Q5815602 / rank @@
+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 @@
+Q5635941
@@ Property / cites work: Q5635941 / rank @@
+Normal rank
@@ Property / cites work @@
+The Mizar Mathematical Library in OMDoc: translation and applications
+Normal rank
@@ Property / cites work @@
+On the rules of suppositions in formal logic
@@ Property / cites work: On the rules of suppositions in formal logic / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
+Normal rank
@@ Property / cites work @@
+Presentation and manipulation of Mizar properties in an Isabelle object logic
+Normal rank
@@ Property / cites work @@
+MizAR 40 for Mizar 40
@@ Property / cites work: MizAR 40 for Mizar 40 / rank @@
+Normal rank
@@ Property / cites work @@
+Merging Procedural and Declarative Proof
@@ Property / cites work: Merging Procedural and Declarative Proof / rank @@
+Normal rank
@@ Property / cites work @@
+Flexary connectives in Mizar
@@ Property / cites work: Flexary connectives in Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+A Mechanized Translation from Higher-Order Logic to Set Theory
+Normal rank
@@ Property / cites work @@
+A Consistent Foundation for Isabelle/HOL
@@ Property / cites work: A Consistent Foundation for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Alternative Aggregates in Mizar
@@ Property / cites work: Alternative Aggregates in Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247084
@@ Property / cites work: Q4247084 / 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 @@
+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 @@
+Accessing the Mizar Library with a Weakly Strict Mizar Parser
+Normal rank
@@ Property / cites work @@
+Partizan Games in Isabelle/HOLZF
@@ Property / cites work: Partizan Games in Isabelle/HOLZF / rank @@
+Normal rank
@@ Property / cites work @@
+Type Inference for ZFH
@@ Property / cites work: Type Inference for ZFH / rank @@
+Normal rank
@@ Property / cites work @@
+On a Practical Way of Describing Formal Deductions
+Normal rank
@@ Property / cites work @@
+Set theory for verification. I: From foundations to functions
+Normal rank
@@ Property / cites work @@
+Topological manifolds
@@ Property / cites work: Topological manifolds / rank @@
+Normal rank
@@ Property / cites work @@
+A logical framework combining model and proof theory
+Normal rank
@@ Property / cites work @@
+Obvious inferences
@@ Property / cites work: Obvious inferences / rank @@
+Normal rank
@@ Property / cites work @@
+The Twelf Proof Assistant
@@ Property / cites work: The Twelf Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945208
@@ Property / cites work: Q4945208 / 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 @@
+Presenting and Explaining Mizar
@@ Property / cites work: Presenting and Explaining Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
+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 @@
+Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
+Normal rank
@@ Property / cites work @@
+The Isabelle Framework
@@ Property / cites work: The Isabelle Framework / 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 @@
+A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
+Normal rank
@@ Property / cites work @@
+Formalization of the fundamental group in untyped set theory using auto2
+Normal rank
@@ Property / DOI @@
+.1007/S10817-018-9479-Z
@@ Property / DOI: 10.1007/S10817-018-9479-Z / rank @@
+Normal rank