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…