Implicit definitions with differential equations for KeYmaera X (system description)

DOI10.1007/978-3-031-10769-6_42OpenAlexW4289104067MaRDI QIDQ2104559

Yong Kiam Tan, Stefan Mitsch, James Gallicchio, André Platzer

Publication date: 7 December 2022

Full work available at URL: https://arxiv.org/abs/2203.01272

zbMATH Keywords

theorem provingdifferential dynamic logicdefinitionsverification of hybrid systems

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Verifying Switched System Stability With Logic ⋮ KeYmaera X

Uses Software

• MetiTarski
• KeYmaera
• RSOLVER
• Benchmarks
• Zenon
• dReal
• HSolver

Cites Work

• Unnamed Item
• Unnamed Item
• MetiTarski: An automatic theorem prover for real-valued special functions
• Differential dynamic logic for hybrid systems
• A complete uniform substitution calculus for differential dynamic logic
• An axiomatic approach to existence and liveness for differential equations
• \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
• Formalization of real analysis: a survey of proof assistants and libraries
• The Complete Proof Theory of Hybrid Systems
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Logical Foundations of Cyber-Physical Systems
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Logical Analysis of Hybrid Systems
• Differential Equation Invariance Axiomatization
• Some undecidable problems involving elementary functions of a real variable
• Hybrid Systems: Computation and Control

This page was built for publication: Implicit definitions with differential equations for KeYmaera X (system description)