KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
Version 5.0.2 provides command line improvements and improved support for interpreted functions in monitoring.
Version 5.0.1 provides bug fixes and a tactic to prepare quantifier elimination queries.
prepareQE with heuristics for equality rewriting, introducing abbreviations, and forming the universal closure of a sequentrcf to complete a query with an external toolqe combines prepareQE and rcf.Version 5.0 provides a definition package for user-defined functions, major parser rewrite, keyboard shortcuts during proofs, tactic performance improvements, and tool improvements.
Definitions: adds support for user-defined functions whose graphs can be implicitly characterized by dL formulas, such as the exponential and trigonometric functions, as solutions of differential equations. Properties of those user-defined functions can be proved using dL's differential equation reasoning principles. A high-level interface for defining functions and non-soundness-critical tactics automate low-level reasoning over implicit characterizations in hybrid system proofs. Builtin definitions that can be used out of the box in models include exp, sin, cos, Pi, and E.
UI: keyboard shortcuts for common proof tasks (customizable through .keymaerax/hotkeys.js file in home directory)
Parser: complete parser re-implementation with support for user-defined functions, full tactic support in web UI parsing
Tactics: performance improvement with builtin forward tactics replacing (some) interpreted tactics
Tools: command line conversion tools from KeYmaera X format to SMT-Lib format (-convert kyx2smt) and Wolfram format (-convert kyx2mat)
Tools: improved Z3-based simplifier
Version 4.9.9 provides UI bug fixes and some tactic performance improvements
Version 4.9.8 provides a security patch and tactic implementation updates:
Version 4.9.7 provides support for switched systems, a fixpoint tactic for hybrid games, as well as UI and robustness improvements:
Version 4.9.6 provides UI and robustness improvements.
Version 4.9.5 provides improved interaction between tactics editing and sequent view.
dC("x^2+y^2=const()", 1)
Version 4.9.4 provides an improved definitions UI to supply proof parameters and modeling assumptions, more robust tactic recording with formula search locators everywhere, tactic branch labels, as well as backend tool and parser updates.
"using", e.g. QE using "x>0 :: x>=0 :: nil"
#...# to identify sub-positions, e.g., dI('R=="x>=0 -> #[{x'=1}]x>=0#")
loop("J", 'R=="[{a;}*]S") <( "Init": r, "Use": s, "Step": t ) to execute tactic r on branch "Init" etc.
e.g., andR('R=="x>=0 & y<=2") <( "x>=0": s, "y<=2": t ) to execute tactic s on branch "x>=0" etc.Version 4.9.3 provides a substantially updated ModelPlex UI and core/parser updates.