FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Uniform Substitution for Differential Game Logic

Author: André Platzer

Paper Information

Title:Uniform Substitution for Differential Game Logic
Authors:André Platzer
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:differential game logic, uniform substitution, axioms, static semantics
Abstract:

ABSTRACT. 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 the soundness of uniform substitution for the monotone modal logic dGL. The resulting axiomatization admits a straightforward modular implementation of dGL in theorem provers.

Pages:16
Talk:Jul 15 17:00 (Session 107D: Logics, Frameworks and Proofs)
Paper: