The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- 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)
- Mechanically proving determinacy of hierarchical block diagram translations (Q2287118) (← links)
- Interaction with formal mathematical documents in Isabelle/PIDE (Q2287890) (← links)
- Beginners' quest to formalize mathematics: a feasibility study in Isabelle (Q2287895) (← links)
- A tale of two set theories (Q2287897) (← links)
- Lemma discovery for induction. A survey (Q2287904) (← links)
- Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL (Q2287906) (← links)
- The Coq library as a theory graph (Q2287907) (← links)
- Inspection and selection of representations (Q2287916) (← links)
- Formalization of function matrix theory in HOL (Q2294128) (← links)
- Solution methods for a min-max facility location problem with regional customers considering closest Euclidean distances (Q2301150) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Priority inheritance protocol proved correct (Q2303234) (← links)
- Solving quantifier-free first-order constraints over finite sets and binary relations (Q2303241) (← 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)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic (Q2305408) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
- Towards bit-width-independent proofs in SMT solvers (Q2305428) (← links)
- A formally verified abstract account of Gödel's incompleteness theorems (Q2305432) (← links)
- Certified equational reasoning via ordered completion (Q2305436) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Classification of finite fields with applications (Q2323448) (← links)
- An Isabelle/HOL formalisation of Green's theorem (Q2323451) (← links)
- A verified compiler from Isabelle/HOL to CakeML (Q2324018) (← links)
- Hierarchical specification and verification of architectural design patterns (Q2324187) (← links)
- Efficient verification of imperative programs using auto2 (Q2324204) (← links)
- Hoare logics for time bounds. A study in meta theory (Q2324211) (← links)
- Model-theoretic conservative extension for definitional theories (Q2333319) (← links)
- Non-standard analysis in dynamic geometry (Q2334581) (← links)
- Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
- Term-generic logic (Q2339466) (← links)
- Infinite executions of lazy and strict computations (Q2347906) (← links)
- Deciding Kleene algebra terms equivalence in Coq (Q2347910) (← links)
- Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Using Isabelle/HOL to verify first-order relativity theory (Q2351148) (← links)
- Reducing higher-order theorem proving to a sequence of SAT problems (Q2351156) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Proof pearl: A mechanized proof of GHC's mergesort (Q2351394) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- Formalization of Shannon's theorems (Q2352494) (← links)
- On the formalization of gamma function in HOL (Q2352499) (← links)
- On the fine-structure of regular algebra (Q2352506) (← links)
- Formalizing complex plane geometry (Q2354913) (← links)
