Buchumschlag

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Hulak, David B., Ramos, Arthur F., de Queiroz, Ruy J. G. B.
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions
von: Hulak, David B., et al.
Veröffentlicht: (2026)

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
von: Hulak, David B., et al.
Veröffentlicht: (2026)

Brownian Motion in Isabelle/HOL
von: Laursen, Christian Pardillo, et al.
Veröffentlicht: (2024)

Linear Programming in Isabelle/HOL
von: Parsert, Julian
Veröffentlicht: (2024)

Verifying Numerical Methods with Isabelle/HOL
von: Bryant, Dustin, et al.
Veröffentlicht: (2025)

Complex Bounded Operators in Isabelle/HOL
von: Unruh, Dominique, et al.
Veröffentlicht: (2025)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
von: Bartl, Lukas, et al.
Veröffentlicht: (2025)

Stalnaker's Epistemic Logic in Isabelle/HOL
von: Guzman, Laura P. Gamboa, et al.
Veröffentlicht: (2024)

Formalization of Differential Privacy in Isabelle/HOL
von: Sato, Tetsuya, et al.
Veröffentlicht: (2024)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL
von: Foster, Simon, et al.
Veröffentlicht: (2024)

Munkres' General Topology Autoformalized in Isabelle/HOL
von: Bryant, Dustin, et al.
Veröffentlicht: (2026)

Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
von: Munive, Jonathan Julián Huerta y, et al.
Veröffentlicht: (2024)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
von: Stübinger, Terru, et al.
Veröffentlicht: (2023)

A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL
von: Schmoetten, Richard, et al.
Veröffentlicht: (2024)

Computational Paths Form a Weak ω-Groupoid
von: Ramos, Arthur F., et al.
Veröffentlicht: (2025)

L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
von: Linzi, Alessandro
Veröffentlicht: (2025)

Formalizing Pick's Theorem in Isabelle/HOL
von: Binder, Sage, et al.
Veröffentlicht: (2024)

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
von: Binder, Sage, et al.
Veröffentlicht: (2026)

Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL
von: Kim, Jinwook
Veröffentlicht: (2026)

The $K_\infty$ Homotopy $λ$-Model
von: Martínez-Rivillas, Daniel O., et al.
Veröffentlicht: (2025)

Solving Homotopy Domain Equations
von: Martínez-Rivillas, Daniel O., et al.
Veröffentlicht: (2021)

Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library
von: Bilotta, Antonella
Veröffentlicht: (2025)

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
von: Ramos, Arthur F., et al.
Veröffentlicht: (2026)

Formalizing MLTL Formula Progression in Isabelle/HOL
von: Kosaian, Katherine, et al.
Veröffentlicht: (2024)

Proof Recommendation System for the HOL4 Theorem Prover
von: Dekhil, Nour, et al.
Veröffentlicht: (2024)

Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
von: Huch, Fabian
Veröffentlicht: (2024)

Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security
von: Kammüller, Florian
Veröffentlicht: (2023)

Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets
von: Atserias, Albert, et al.
Veröffentlicht: (2024)

Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model
von: Martinez-Rivillas, Daniel O., et al.
Veröffentlicht: (2026)

Well-Founded Coalgebras Meet König's Lemma
von: Urbat, Henning, et al.
Veröffentlicht: (2025)

Affine Disjunctive Invariant Generation with Farkas' Lemma
von: Ke, Jingyu, et al.
Veröffentlicht: (2023)

A Beluga Formalization of the Harmony Lemma in the $π$-Calculus
von: Cecilia, Gabriele, et al.
Veröffentlicht: (2024)

Mechanized HOL Reasoning in Set Theory
von: Guilloud, Simon, et al.
Veröffentlicht: (2024)

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
von: Peled, Romy, et al.
Veröffentlicht: (2025)

Lemmas: Generation, Selection, Application
von: Rawson, Michael, et al.
Veröffentlicht: (2023)

On the Formalization of Network Topology Matrices in HOL
von: Aksoy, Kubra, et al.
Veröffentlicht: (2026)

Meaning as Use, Application, Employment, Purpose, Usefulness
von: de Queiroz, Ruy J. G. B.
Veröffentlicht: (2025)

From the Notebooks to the Investigations and Beyond
von: de Queiroz, Ruy J. G. B.
Veröffentlicht: (2025)

Lemmanaid: Neuro-Symbolic Lemma Conjecturing
von: Alhessi, Yousef, et al.
Veröffentlicht: (2025)

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
von: Civini, Emanuele, et al.
Veröffentlicht: (2026)