zbMATH — the first resource for mathematics

KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. (English) Zbl 06515530
Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-21400-9/pbk; 978-3-319-21401-6/ebook). Lecture Notes in Computer Science 9195. Lecture Notes in Artificial Intelligence, 527-538 (2015).
Summary: KeYmaera X is a theorem prover for differential dynamic logic (\(\mathsf d \mathcal L\)), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems models requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute these tactics in parallel, and interface with partial proofs via an extensible user interface. Advanced proof search features – and user-defined tactics in particular – are difficult to check for soundness. To admit extension and experimentation in proof search without reducing trust in the prover, KeYmaera X is built up from a small trusted kernel. The prover kernel contains a list of sound \(\mathsf d \mathcal L\) axioms that are instantiated using a uniform substitution proof rule. Isolating all soundness-critical reasoning to this prover kernel obviates the intractable task of ensuring that each new proof search algorithm is implemented correctly. Preliminary experiments suggest that a single layer of tactics on top of the prover kernel provides a rich language for implementing novel and sophisticated proof search techniques.
For the entire collection see [Zbl 1316.68011].

03B35 Mechanization of proofs and logical operations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI