Products

Deepire-2.0-HO

🔔 ML-based clause selection guidance for TPTP’s HO dialects in Vampire.

• Vampire with HO support: developed by Bhayat as a fork of master in 2022 at GitHub
• Vampire with Deepire-2.0-HO support at GitHub
• Training infracture for training Deepire models at GitHub

λENIGMA

🔔 ML-based clause selection guidance for TPTP’s HO dialects in E Prover.

• E Prover with λENIGMA support at GitHub
• Training infracture for training ENIGMA models at GitHub
• Bug reports and fixes discovered in E on Isabelle export. See files bug00N-*.md for N ∈ {1,2,3,4}.

RamParILS

🔔 Parallelized automated algorithm configuration via Iterated Local Search.

• Parallel Rust rewrite of ParamILS
• Web page with documentation
• Source codes at GitHub

Vizabelle

🔔 Visualization tool to inspect TPTP proofs of Isabelle Sledgehammer exports.

• Source codes at GitHub
• Library with Isabelle ATP proof examples.

DHORES

🔔 Prototype Higher-Order Resolution Prover Supporting Dependent HOL.

• Source codes available for download

DLash

🔔 Dependent Higher-order Logic Prover DLash.

• Source codes available for download