A complete uniform substitution calculus for differential dynamic logic

DOI10.1007/s10817-016-9385-1zbMath1437.03119DBLPjournals/jar/Platzer17arXiv1601.06183OpenAlexW3101115050WikidataQ59611679 ScholiaQ59611679MaRDI QIDQ1707599

André Platzer

Publication date: 3 April 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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

zbMATH Keywords

axiomatizationdifferentialsaxiomsuniform substitutiondifferential dynamic logicstatic semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (18)

Relational Differential Dynamic Logic ⋮ Skill-Based Verification of Cyber-Physical Systems ⋮ Constructive Game Logic ⋮ Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Verification of Hybrid Systems ⋮ Pegasus: sound continuous invariant generation ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Verifying Switched System Stability With Logic ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ From post-conditions to post-region invariants ⋮ Verifiably safe exploration for end-to-end reinforcement learning ⋮ Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems ⋮ Deductive stability proofs for ordinary differential equations ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ Verified interactive computation of definite integrals ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ Uniform substitution at one Fell swoop ⋮ Implicit definitions with differential equations for KeYmaera X (system description)

Uses Software

• KeYmaera
• KeYmaera X

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• HRELTL: a temporal logic for hybrid systems
• Differential dynamic logic for hybrid systems
• Theorem proving modulo
• The Complete Proof Theory of Hybrid Systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• A Uniform Substitution Calculus for Differential Dynamic Logic
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• The Structure of Differential Invariants and Differential Cut Elimination
• Differential Game Logic
• Differential Hybrid Games
• Banishing the rule of substitution for functional variables
• Classes of Recursively Enumerable Sets and Their Decision Problems

This page was built for publication: A complete uniform substitution calculus for differential dynamic logic