A complete uniform substitution calculus for differential dynamic logic

DOI10.1007/S10817-016-9385-1zbMATH Open1437.03119DBLPjournals/jar/Platzer17arXiv1601.06183OpenAlexW3101115050WikidataQ59611679 ScholiaQ59611679MaRDI QIDQ1707599FDOQ1707599

Authors: André Platzer 

Publication date: 3 April 2018

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

Abstract: This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms, which uniform substitutions instantiate soundly. The static semantics of differential dynamic logic and the soundness-critical restrictions it imposes on proof steps is captured exclusively in uniform substitutions and variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this article introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivatives as first-class axioms to reason about differential equations axiomatically. The resulting axiomatization of differential dynamic logic is proved to be sound and relatively complete.

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

Recommendations

• A uniform substitution calculus for differential dynamic logic
• Uniform substitution for differential game logic
• Dynamic logic as a uniform framework for theorem proving in intensional logic
• Differential dynamic logic for hybrid systems
• A calculus of substitutions for DPL

zbMATH Keywords

axiomatizationaxiomsdifferentialsuniform substitutiondifferential dynamic logicstatic semantics

Mathematics Subject Classification ID

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

Cites Work

• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Differential dynamic logic for hybrid systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logical frameworks
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem proving modulo
• Classes of Recursively Enumerable Sets and Their Decision Problems
• Banishing the rule of substitution for functional variables
• 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
• The structure of differential invariants and differential cut elimination
• HRELTL: a temporal logic for hybrid systems
• Title not available (Why is that?)
• Differential Hybrid Games
• Differential game logic

Cited In (29)

• Differential equation invariance axiomatization
• Schematic program proofs with abstract execution. Theory and applications
• An axiomatic approach to existence and liveness for differential equations
• Constructive game logic
• Implicit definitions with differential equations for KeYmaera X (system description)
• Skill-based verification of cyber-physical systems
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Relational differential dynamic logic
• \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
• A uniform substitution calculus for differential dynamic logic
• Deductive stability proofs for ordinary differential equations
• Differential equation axiomatization. The impressive power of differential ghosts
• \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
• Pegasus: sound continuous invariant generation
• Verification of Hybrid Systems
• Verified interactive computation of definite integrals
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Title not available (Why is that?)
• 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
• Uniform substitution for differential game logic
• Dynamical properties of logical substitutions
• Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
• Uniform substitution at one Fell swoop
• An axiomatic approach to liveness for differential equations
• Parallel composition and modular verification of computer controlled systems in differential dynamic logic
• Bellerophon: tactical theorem proving for hybrid systems
• Verifying Switched System Stability With Logic

Uses Software

• KeYmaera
• KeYmaera X

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1707599)