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