A verified prover based on ordered resolution.

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel

Browse the full CPP paper archive.