Error with derived axioms database in KeYmaera 5.0.2
ytzemih opened this issue · 2 comments
Hi, I'm running KeYmaera X 5.0.2 on my Ubuntu 22.04 machine (plain, just using Z3). I've completely removed the ~/.keymaerax directory to also avoid clearing the cache. But the error remains, only the line about "Clearing your cache" is gone. It seems that my Java version is alright. Assuming that this type of error might be somewhat concerning despite its about derived axioms. I thank you for some help.
[launcher] Restarting KeYmaera X with sufficient stack space
/usr/lib/jvm/java-17-openjdk-amd64/bin/java -Xss20M -da -jar keymaerax.jar -launch -ui
WARNING: sun.reflect.Reflection.getCallerClass is not supported. This will impact performance.
[launcher] Database version: 4.8.0
Clearing your cache because of an update.
Error deriving axioms, KeYmaera X continues with restricted functionality; details: WARNING: Encountered 19 errors when trying to populate DerivedAxioms database. Unable to derive:
timesDivInverse
powNegOne
powerLemma
timesPowersBoth
powerEven
powerOdd
divideNumber
divideRat
divideNeg
normalizeCoeff0
powerDivideEven
powerDivideOdd
ratFormAdd
ratFormMinus
ratFormDivide
ratFormTimes
ratFormNeg
taylorModelPowerEven
taylorModelPowerOdd
As far as I know, Z3 is unable to prove all the derived axioms by itself. However, setting AXIOM_DERIVE_TIMEOUT to a higher value (for example 30 for 30 seconds) in your keymaerax.conf might allow Z3 to prove at least some more axioms.
Mathematica with a sufficiently high timeout is able to prove all derived axioms, though the default timeout is maybe a bit too short.