Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, Andre Platzer,
"KeYmaera X - An Axiomatic Tactical Theorem Prover for Hybrid Systems"
: Automated Deduction - CADE-25 (25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings), Serie Lecture Notes in Computer Science (LNCS), Vol. 9195, Springer, Seite(n) 527-538, 2015, ISBN: 978-3-319-21400-9
Original Titel:
KeYmaera X - An Axiomatic Tactical Theorem Prover for Hybrid Systems
Sprache des Titels:
Englisch
Original Buchtitel:
Automated Deduction - CADE-25 (25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings)
Original Kurzfassung:
KeYmaera X is a theorem prover for differential dynamic logic (dL), 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 dL 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.
Forschungs-