"A Complete Semantic Back Chaining Proof System."

Xumin Nie, David A. Plaisted (1990)
a service of Schloss Dagstuhl - Leibniz Center for Informatics