Cтраница 4
Подсказка: то, что Ахилл считает правилом вывода, Черепаха fyT же превращает в простую строчку системы. [46]
Особенность этих логик состоит в использовании в правилах вывода конкретных знаний о свойствах отношений внутри предметных областей. [47]
В предыдущей главе мы рассматривали метод резолюций как правило вывода, которое может быть использовано для порождения новых дизъюнктов из уже имеющихся. Мы видели также, что неограниченное применение резолюции может порождать много лишних и ненужных дизъюнктов наряду с полезными. Хотя можно использовать стратегию выбрасывания, чтобы выбросить некоторые из этих ненужных и бесполезных дизъюнктов после того, как они порождены, на их порождение уже будет потеряно время. Далее, если порождены бесполезные дизъюнкты, то нужны большие ресурсы машинного времени и памяти для того, чтобы определить, что эти дизъюнкты действительно лишние и ненужные. Поэтому для получения эффективных процедур доказательства теорем мы должны не допустить порождения большого числа бесполезных дизъюнктов. Это приводит к обсуждению стратегий резолюции. [48]
РЕЗОЛЮЦИЯ [ resolution ] В исчислении предикатов - правило вывода, используемое для вывода новой логической формулы из двух посылок. Резолюции применяются при автоматическом построении доказательств и в экспертных системах. [49]