"Soundness of Q-resolution with dependency schemes."

Friedrich Slivovsky, Stefan Szeider (2016)
a service of Schloss Dagstuhl - Leibniz Center for Informatics