The following pages link to Isabelle/Isar (Q14553):
Displayed 50 items.
- Improving legibility of formal proofs based on the close reference principle is NP-hard (Q286805) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- A certified proof of the Cartan fixed point theorems (Q438546) (← links)
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (Q670696) (← links)
- Amortized complexity verified (Q670702) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- Mathematical method and proof (Q857692) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- A mechanized proof of the basic perturbation lemma (Q928666) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- A UTP semantic model for Orc language with execution status and fault handling (Q1633048) (← links)
- A formally verified proof of the central limit theorem (Q1694568) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Towards verified handwritten calculational proofs (short paper) (Q1791183) (← links)
- A formally verified solver for homogeneous linear Diophantine equations (Q1791187) (← links)
- Towards formal foundations for game theory (Q1791194) (← links)
- Theories as types (Q1799118) (← links)
- A comparison of Mizar and Isar (Q1868515) (← links)
- A generic and executable formalization of signature-based Gröbner basis algorithms (Q2028994) (← links)
- Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
- Relational characterisations of paths (Q2210868) (← links)
- Interpreting mathematical texts in Naproche-SAD (Q2219411) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Interaction with formal mathematical documents in Isabelle/PIDE (Q2287890) (← links)
- Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL (Q2287906) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
- Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
- Using Isabelle/HOL to verify first-order relativity theory (Q2351148) (← links)
- Locales: a module system for mathematical theories (Q2352487) (← links)
- From LTL to deterministic automata. A safraless compositional approach (Q2363815) (← links)
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (Q2364696) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book (Q2462639) (← links)
- Proving pointer programs in higher-order logic (Q2486585) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Translating Scala Programs to Isabelle/HOL (Q2817953) (← links)
- Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0 (Q2819200) (← links)
- Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems (Q2843039) (← links)
- From Tarski to Hilbert (Q2849509) (← links)
- An Isabelle Proof Method Language (Q2879265) (← links)
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving (Q2881098) (← links)
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL (Q2914756) (← links)
- Automated Reasoning in Higher-Order Regular Algebra (Q2915136) (← links)
- Improving legibility of natural deduction proofs is not trivial (Q2921120) (← links)
- UTPCalc — A Calculator for UTP Predicates (Q2971182) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- Dependently-Typed Formalisation of Relation-Algebraic Abstractions (Q3007580) (← links)