The following pages link to Isar (Q16770):
Displaying 50 items.
- Four decades of {\textsc{Mizar}}. Foreword (Q286794) (← links)
- Improving legibility of formal proofs based on the close reference principle is NP-hard (Q286805) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- An inductive approach to strand spaces (Q470008) (← links)
- Structured derivations: a unified proof style for teaching mathematics (Q607406) (← links)
- Tactics for hierarchical proof (Q626933) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Automated theorem provers: a practical tool for the working mathematician? (Q657585) (← links)
- Computer theorem proving in mathematics (Q704001) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- Balancing the load. Leveraging a semantics stack for systems verification (Q835780) (← links)
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps (Q839032) (← links)
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (Q841684) (← links)
- Quantum non-Markovian stochastic equations (Q843811) (← links)
- Mathematical method and proof (Q857692) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- A mechanized proof of the basic perturbation lemma (Q928666) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- Generating certified code from formal proofs: a case study in homological algebra (Q968307) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Fractional generalization of the quantum Markovian master equation (Q1034411) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- A UTP semantic model for Orc language with execution status and fault handling (Q1633048) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- Foundational (co)datatypes and (co)recursion for higher-order logic (Q1687535) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Flexary connectives in Mizar (Q1749141) (← links)
- A comparison of Mizar and Isar (Q1868515) (← links)
- A generic and executable formalization of signature-based Gröbner basis algorithms (Q2028994) (← links)
- The Isabelle/Naproche natural language proof assistant (Q2055899) (← links)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
- Relational characterisations of paths (Q2210868) (← links)
- Bridging the gap between argumentation theory and the philosophy of mathematics (Q2271079) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- First steps towards a formalization of forcing (Q2333671) (← links)
- Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
- Using Isabelle/HOL to verify first-order relativity theory (Q2351148) (← links)
- Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets (Q2352482) (← links)
- Formalizing complex plane geometry (Q2354913) (← links)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
- Formalizing provable anonymity in Isabelle/HOL (Q2355379) (← links)
