The following pages link to Isabelle (Q13212):
Displaying 50 items.
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- Affine systems of ODEs in Isabelle/HOL for hybrid-program verification (Q2038037) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- Integration of formal proof into unified assurance cases with Isabelle/SACM (Q2065527) (← links)
- Random belief system dynamics in complex networks under time-varying logic constraints (Q2068428) (← links)
- Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem (Q2069874) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Logic-independent proof search in logical frameworks (short paper) (Q2096460) (← links)
- A formalization of Dedekind domains and class groups of global fields (Q2102929) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
- A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
- \textsc{Prawf}: an interactive proof system for program extraction (Q2106598) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle (Q2119971) (← links)
- Strong eventual consistency of the collaborative editing framework WOOT (Q2121065) (← links)
- A unified framework for the computational comparison of adaptive mesh refinement strategies for all-quadrilateral and all-hexahedral meshes: locally adaptive multigrid methods versus h-adaptive methods (Q2124328) (← links)
- A modular first formalisation of combinatorial design theory (Q2128787) (← links)
- Beautiful formalizations in Isabelle/Naproche (Q2128789) (← links)
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL (Q2128791) (← links)
- CICM'21 systems entries (Q2128833) (← links)
- The undecidability of proof search when equality is a logical connective (Q2134939) (← links)
- The role of entropy in guiding a connection prover (Q2142077) (← links)
- Automated verification of the parallel Bellman-Ford algorithm (Q2145339) (← links)
- Shedding new light on the foundations of abstract argumentation: modularization and weak admissibility (Q2163881) (← links)
- Mechanised assessment of complex natural-language arguments using expressive logic combinations (Q2180221) (← links)
- Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL (Q2180230) (← links)
- Verifying randomised social choice (Q2180231) (← links)
- Certification of nonclausal connection tableaux proofs (Q2180504) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- Formal reasoning under cached address translation (Q2209539) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- Relational characterisations of paths (Q2210868) (← links)
- A framework for formal dynamic dependability analysis using HOL theorem proving (Q2219384) (← links)
- Induction with generalization in superposition reasoning (Q2219385) (← links)
- Simple dataset for proof method recommendation in Isabelle/HOL (Q2219413) (← links)
- Certifying proofs in the first-order theory of rewriting (Q2233502) (← links)
- Fundamentals of logic and computation. With practical automated reasoning and verification (Q2240968) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Modal Kleene algebra applied to program correctness (Q2281640) (← links)
- An algebra of synchronous atomic steps (Q2281642) (← links)
- Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8--12, 2019. Proceedings (Q2282174) (← links)
- Relational data across mathematical libraries (Q2287899) (← links)
- MMTTeX: connecting content and narration-oriented document formats (Q2287910) (← links)
- Diagram combinators in MMT (Q2287911) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Priority inheritance protocol proved correct (Q2303234) (← links)
- Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (Q2303242) (← links)
- A verified implementation of algebraic numbers in Isabelle/HOL (Q2303244) (← links)
