Метод Хао Вонга

[kernel1983]

Здравствуйте.
Требуется доказать клаузу, используя алгоритм Вонга: $AB, A \to C \vdash CB$. Исключаю импликацию и конъюнкцию: $A, B, \neg A \vee C \vdash CB$. Разбиваю на две клаузы: 1) $A, B, \neg A \vdash CB$, 2) $A, B, C \vdash CB$. В первом случае переношу букву с отрицанием в другую часть, снимая отрицание: $A, B, \vdash CB, A$. Вторую клаузу оставляю без изменений. Но что это даёт? В правой части должна быть дизъюнкция, в крайнем случае, вида $X \vee 0$. Подскажите, пожалуйста.
Есть ли литература на русском языке, где всё это доступно описано?
Спасибо.