Метод - резолюция
Cтраница 4
Тогда ( Su / C) - противоречивое множество, что может быть доказано методом резолюции. [46]
Следствие 1.5. Если множество S формул невыполнимо, то этот факт всегда можно установить методом резолюций. [47]
В [20] дан анализ результатов применения логико-управляемой системы, в которой для планирования действий робота был использован метод резолюций совместно с механизмом забывания фактов. Но предложенная еще в [19] комбинация метода резолюций и процедуры забывания в общем случае оказалась внелогической. [48]
 |
Граф опровержения для системы формул. [49] |
Доказательство, что S0 есть логическое следствие аксиом н фактов, может быть выполнено, например, методом резолюций. [50]
Хотя этот процесс кажется таинственным, в действительности он сводится к рассуждению от цели, реализованному с помощью метода резолюции. [51]
Существенное продвижение в этом направлении предпринял Грин [11], продемонстрировавший в качестве генератора планов законченную систему доказательства теорем методом резолюции. Согласно этому подходу, начальная ситуация, целевая ситуация и результаты применения имеющихся операторов описываются в виде множества аксиом исчисления предикатов первого порядка. Далее с помощью принципа резолюции доказывается предположение, что существует ситуация, удовлетворяющая описанию цели. Побочным результатом успешно проведенного доказательства является план последовательного преобразования начальной ситуации в целевую. [52]
Страницы: 1 2 3 4