We are happy to present a collection of software tools developed by our team, spanning ML-guided theorem proving, algorithm configuration, proof visualization, and higher-order logic reasoning. See our Products page for downloads and source code.
-
Deepire-2.0-HO — ML-based clause selection guidance for TPTP’s higher-order dialects in the Vampire prover, extending the Deepire learning framework to the higher-order setting.
-
λENIGMA — ML-based clause selection guidance for TPTP’s higher-order dialects in the E prover, bringing ENIGMA’s learning-guided search to higher-order logic, including bug reports and fixes discovered during evaluation on Isabelle exports.
-
RamParILS — A parallelized Rust rewrite of ParamILS for automated algorithm configuration via Iterated Local Search, significantly speeding up hyperparameter tuning for automated reasoning tools.
-
Vizabelle — A visualization tool for inspecting TPTP proofs produced by Isabelle Sledgehammer exports, with an online library of ATP proof examples.
-
DHORES — A prototype higher-order resolution prover with support for Dependent Higher-Order Logic (DHOL).
-
DLash — A dependent higher-order logic prover implementing the DLash calculus.