1 citations · 1 across the 1 of their papers we have counts for
1 paper
Lukas Bartl, Jasmin Blanchette, Tobias Nipkow
Metis is an ordered paramodulation prover built into the Isabelle/HOL proof assistant. It attempts to close the current goal using a given list of lemmas. Typically these lemmas ar…