Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann

Browse the full CADE paper archive.