This certainly looks worth doing! Larry > On 28 Sep 2020, at 09:25, Jasmin Blanchette <[email protected]> wrote: > > I don't think it should influence the schedule, but Isabelle2021 would be > high time to repackage new versions of the automatic theorem provers and new > provers -- and make sure that things work smoothly with Sledgehammer. > > Main provers to update: > > E > Vampire > CVC4 > > New provers: > > veriT > Zipperposition > > All of these now partly or fully support higher-order logic. The main > bottleneck here is that I've lost my Windows installation and I need to do > something about this very soon (i.e., find somebody else who can own that > problem or reinstall Windows myself). > > (On a related note, Martin D. has recently updated Metis's source code, which > is nice because Metis had some completeness bugs. We don't know if it > affected Isabelle users but that could have explained why it sometimes went > seemingly forever on seemingly easy goals.)
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
