<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 presents a uniform substitution calculus for differential game logic (dGL). Church's uniform substitutions substitute a term or formula for a function or predicate symbol everywhere. After generalizing them to differential game logic and allowing for the substitution of hybrid games for game symbols, uniform substitutions make it possible to only 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 axiomatization adopts only a finite number of ordinary dGL formulas as axioms, which uniform substitutions instantiate soundly. This paper proves soundness and completeness of uniform substitutions for the monotone modal logic dGL. The resulting axiomatization admits a straightforward modular implementation of dGL in theorem provers.
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), Computer Science - Computer Science and Game Theory, FOS: Mathematics, F.4.1, F.3.2, 03F03, 03B70, 34A38, 91A25, F.3.1, F.4.1; F.3.1; F.3.2; I.2.3, Logic (math.LO), Computer Science and Game Theory (cs.GT), 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), Computer Science - Computer Science and Game Theory, FOS: Mathematics, F.4.1, F.3.2, 03F03, 03B70, 34A38, 91A25, F.3.1, F.4.1; F.3.1; F.3.2; I.2.3, Logic (math.LO), Computer Science and Game Theory (cs.GT), 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). | 6 | |
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. | Average | |
influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |