доказательство теорем на
основе принципа резолюции
Литература
Waterman and Hayes-Roth (1978) - классическая книга по системам, управляемым образцами. В книге Nilsson (1980) можно найти фундаментальные понятия, относящиеся к задаче автоматического доказательства теорем, включая алгоритм преобразования логических формул в конъюнктивную нормальную форму. Прологовская программа для выполнения этого преобразования приведена в Clocksin and Mellish (1981).
Clocksin F. W. and Mellish С S. (1981).
Nilsson N. J. (1980).
Waterman D. A. and Hayes-Roth F. (1978, eds).
Назад | Содержание | Вперёд
Назад | Содержание | Вперёд
ОТВЕТЫ К НЕКОТОРЫМ УПРАЖНЕНИЯМ
Глава 1
1. 1
(a) no
(b) X = пат
(c) X = боб
(d) X = боб, Y = пат
1. 2
(a) ?- родитель( X, пат).
(b) ?- родитель( лиз, X).
(c) ?- родитель( Y, пат), родитель( X, Y).
1. 3
(a) счастлив( X) :-
родитель( X, Y).
(b) имеетдвухдетей( X) :-
родитель( X, Y),
сестра( Z, Y).
1. 4
внук( X, Z) :-
родитель( Y, X),
родитель( Z, Y).
1. 5
тетя( X, Y) :-
родитель( Z, Y),
сестра( X, Z).
1. 6
Да. (Определение верно)
1. 7
(a) возвратов не будет
(b) возвратов не будет
(c) возвратов не будет
(d) возвраты будут
Глава 2
