Skip to content

Version 5.0
Compare
Choose a tag to compare
@smitsch smitsch released this 11 Aug 08:30
· 644 commits to master since this release
5.0
This tag was signed with the committer’s verified signature.
LSLabBuild
GPG key ID: 9C461005FDEDB15E
Learn about vigilant mode.
8774fde

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

Assets 3
Loading