<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>
This paper introduces a new 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 rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of nontrivial schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms. The static semantics of differential dynamic logic is captured exclusively in uniform substitutions and bound variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this paper introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivations as first-class axioms in dL.
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, I.2.3, Computer Science - Programming Languages, Mathematics - Logic, Logic in Computer Science (cs.LO), FOS: Mathematics, F.4.1, F.3.2, 03F03, 03B70, 34A38, 89999 Information and Computing Sciences not elsewhere classified, F.3.1, F.4.1; F.3.1; F.3.2; I.2.3, Logic (math.LO), Programming Languages (cs.PL)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, I.2.3, Computer Science - Programming Languages, Mathematics - Logic, Logic in Computer Science (cs.LO), FOS: Mathematics, F.4.1, F.3.2, 03F03, 03B70, 34A38, 89999 Information and Computing Sciences not elsewhere classified, F.3.1, F.4.1; F.3.1; F.3.2; I.2.3, Logic (math.LO), Programming Languages (cs.PL)
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 21 | |
popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |