"A Semantic Backward Chaining Proof System."

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