"Renaming a Set of Non-Horn Clauses."

Xumin Nie, Qing Guo (2000)
a service of Schloss Dagstuhl - Leibniz Center for Informatics