A Modular Formalization of Superposition in Isabelle/HOL.

Martin Desharnais, Balzs Tth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret

Browse the full ITP paper archive.