nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Uniform Substitution for Differential Game Logic

verfasst von : André Platzer

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper presents a uniform substitution calculus for differential game logic (

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq1_HTML.gif

). 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

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq2_HTML.gif

formulas as axioms, which uniform substitutions instantiate soundly. This paper proves soundness and completeness of uniform substitutions for the monotone modal logic

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq3_HTML.gif

. The resulting axiomatization admits a straightforward modular implementation of

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq4_HTML.gif

in theorem provers.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued Logic

Nächstes Kapitel A Logical Framework with Commutative and Non-commutative Subexponentials

The addition of games to the previous

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq23_HTML.gif

prover was more complex [10], with an implementation effort measured in months not minutes. Unfortunately, this is not quite comparable, because both provers implement markedly different flavors of games for hybrid systems. The game logic for

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq24_HTML.gif

[10] was specifically tuned as an exterior extension to be more easily implementable than

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq25_HTML.gif

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq26_HTML.gif

Even if not critical here, differentials have a differential-form semantics [6] as the sum of all partial derivatives by

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq137_HTML.gif

multiplied by the corresponding values of

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq138_HTML.gif

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq139_HTML.gif

A logic L closed under first-order connectives is differentially expressive (for

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq645_HTML.gif

) if every

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq646_HTML.gif

formula \(\phi \) has an equivalent

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq648_HTML.gif

in L and all differential equation equivalences of the form

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_15/464406_1_En_15_IEq649_HTML.gif

for G in L are provable in its calculus.

Bohrer, B., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: Bertot, Y., Vafeiadis, V. (eds.) CPP. ACM (2017). https://doi.org/10.1145/3018610.3018616

Church, A.: Introduction to Mathematical Logic. Princeton University Press, Princeton (1956)MATH

Fulton, N., Mitsch, S., Quesel, J.D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A., Middeldorp, A. (eds.) CADE. LNCS, vol. 9195, pp. 527–538. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-21401-6_36CrossRef

Parikh, R.: Propositional game logic. In: FOCS, pp. 195–200. IEEE (1983). https://doi.org/10.1109/SFCS.1983.47

Platzer, A.: Differential game logic. ACM Trans. Comput. Log. 17(1), 1:1–1:52 (2015). https://doi.org/10.1145/2817824MathSciNetCrossRefMATH

Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas. 59(2), 219–265 (2017). https://doi.org/10.1007/s10817-016-9385-1MathSciNetCrossRefMATH

Platzer, A.: Differential hybrid games. ACM Trans. Comput. Log. 18(3), 19:1–19:44 (2017)MathSciNetCrossRef

Platzer, A.: Uniform substitution for differential game logic. CoRR abs/1804.05880 (2018)

Platzer, A., Quesel, J.D.: KeYmaera: a hybrid theorem prover for hybrid systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR. LNCS, vol. 5195, pp. 171–178. Springer, Berlin (2008). https://doi.org/10.1007/978-3-540-71070-7_15CrossRef

10.

Quesel, J.-D., Platzer, A.: Playing hybrid games with KeYmaera. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 439–453. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_34CrossRef

11.

Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)MATH

Titel: Uniform Substitution for Differential Game Logic
verfasst von: André Platzer
Verlag: Springer International Publishing
Buch: Automated Reasoning
Print ISBN: 978-3-319-94204-9

Electronic ISBN: 978-3-319-94205-6

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94205-6_15

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"