Опровержение резолюций
В языке PROLOG используется "интерпретация фраз Хорна для решения проблем" (см. [Kowalski, 1979, р. 88-89]). Фундаментальный метод доказательства теорем, на котором базируется PROLOG, называется опровержением резолюций (resolution refutation). Полное описание этого метода читатель найдет в книге Робинсона [Robinson, 1979], а в этом разделе мы попытаемся кратко изложить только основные идеи.
