zbMATH — the first resource for mathematics

Uniform substitution at one Fell swoop. (English) Zbl 07178990
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer (ISBN 978-3-030-29435-9/pbk; 978-3-030-29436-6/ebook). Lecture Notes in Computer Science 11716. Lecture Notes in Artificial Intelligence, 425-441 (2019).
Summary: Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical admissibility checks, this paper introduces a uniform substitution mechanism that proceeds in a linear pass homomorphically along the formula. Soundness is recovered using a simple variable condition at the replacements performed by the substitution. The setting in this paper is that of differential hybrid games, in which discrete, continuous, and adversarial dynamics interact in differential game logic \(\text sf{dGL}\). This paper proves soundness and completeness of one-pass uniform substitutions for \(\text sf{dGL}\).
For the entire collection see [Zbl 1428.68018].
03B35 Mechanization of proofs and logical operations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
KeY; KeYmaera
Full Text: DOI