Навигация
3.3 Принцип резолюций
Мы стараемся упростить синтаксис исчисления таким образом, чтобы уменьшить количество правил влияния, необходимое для доказательства теорем. Вместо дюжины или более правил, которые используются при доказательстве теорем вручную, системы автоматического доказательства для фразовых форм используют единственное правило вывода — принцип резолюций, — впервые описанное Робинсоном ([Robinson, 1965]).
Рассмотрим следующий пример из исчисления высказываний. В дальнейшем прописными буквами Р, Q, R,... будут обозначаться отдельные фразы, а строчными греческими U, ф и £ — пропозициональные переменные, как и раньше.
Если U и ф представляют две произвольные фразы, которые можно представить в конъюнктивной нормальной форме, и
U={ U1, ..., Ui, ...., Um},
и
ф= {ф1..., фi.....,фn}, и
Ui, = ¬фi при 1[i[mm,1 [j [ n,
то новую фразу £ можно вывести из объединения U' и ф', где
U' = U¬{ Ui} и ф' = ф¬{ф,}.
Фраза £ = U' и ф' называется резольвентой шага резолюции, а U и ф являются родительскими фразами. Иногда говорят, что U и ф "сталкиваются" на паре дополняющих литералов Ui , и фj.
Мощность резолюции обеспечивается тем, что в ней суммируется множество других правил. Это станет очевидно после того, как обычные правила будут представлены в конъюнктивной нормальной форме.
В левой колонке табл. 1 перечислены наименования правил вывода, в средней показано, как они выглядят в обычных обозначениях, а в правой колонке — во фразовой форме. В каждой записи выражения в верхней части представляют схему предпосылок, а выражения в нижней части — схему заключений. Из этой таблицы видно, что каждое из цитированных выше пяти правил является одним из экземпляров резолюции:
Таблица 1. Обобщение резолюции.
| Правило вывода | Обычная форма | Конъюнктивная нормальная форма | ||
| Modus ponens | (U | {¬U,Ф},{U}/{ф} | ||
| Modus fallens | (U | {¬U,ф},{-,ф}/{-U} | ||
| Сцепление | (U | {¬U,ф},{¬ф,£}/{¬U,£} | ||
| Слияние | (U | {U,ф},{¬U,ф}/{ф} | ||
| Reductio | (U,¬U)/ | | {¬U},{U}/{} |
ф,U)/ФПротиворечие в правиле, которое обычно обозначается значком 1, дает в результате пустую фразу— {}. Это означает, что предпосылки несовместимы. Если считать, что предпосылки описывают некоторое состояние предметной области, то такой набор предпосылок не может быть реально обеспечен в ней, т.е. такое состояние невозможно.
Главное, что компонент автоматического доказательства теорем, который является основным компонентом большинства систем искусственного интеллекта и, в частности, языков программирования искусственного интеллекта, таких как PROLOG, является системой, опровержения резолюций. Для того чтобы доказать, что р следует из некоторого описания состояния (или теории) Т, нужно положить —р и попытаться доказать, что из этого предположения следует утверждение, противоречащее Т. Если это удастся сделать, то тем самым подтверждается утверждение р, а в противном случае оно опровергается.
В исчислении предикатов использование резолюций требует дополнительных усилий, поскольку в этом исчислении присутствуют переменные. Основная операция сопоставления в доказательстве теорем с помощью резолюций называется унификацией. При сопоставлении дополняющих литералов отыскивается такая подстановка переменных, которая превращает оба выражения в идентичные.
Например, выражения БЕЖИТ_БЫСТРЕЕ_ЧЕМ(Х, улитка) и БЕЖИТ_БЫСТРЕЕ _ЧЕМ (черепаха, Y) превращаются в идентичные при подстановке {Х/черепаха, Y/улитка}. Такая подстановка называется унификатором. Наша цель — отыскать наиболее общую подстановку такого рода.
Похожие работы
... задач и выдвигать гипотезы , которые могут быть подтверждены или опровержены. Знания могут быть получены в процессе наблюдения за каким-либо объектогм. Режимы работы инженера по знаниям, консультолога в процессе приобретения знаний. протокольный анализ записываются рассуждения вслух в процессе решения задач. О.с. составляются протоколы, которые анализируются Интервью - ведется диалог с ...
... философии - особенно с методологических позиций материалистического понимания истории и материалистической диалектики с учетом социокультурной обусловленности этого процесса. Однако в западной философии и методологии науки XX в. фактически - особенно в годы «триумфального шествия» логического позитивизма (а у него действительно были немалые успехи) - научное знание исследовалось без учета его ...
... субъекта (Юм), априорным формам мышления (Кант), целевым установкам личности (прагматизм), интерсубъективным конвенциям (А. Пуанкаре) и др. Фундаментальными проблемами в данной сфере выступали в классической философии проблема критерия И., трактовка которого соответствовала принятому определению И. (от эйдотического образца у Платона до Божественной Мудрости у Фомы Аквинского, с одной стороны, и ...
описания знания подразделяются на: 1) Декларативные (факты) - это знания вида “А есть А”. 2) Процедурные - это знания вида “Если А, то В”. Декларативные знания подразделяются на объекты, классы объектов и отношения. Объект - это факт, который задается своим значением. Класс объектов - это имя, под которым объединяется конкретная совокупность объектов-фактов. Отношения - определяют связи ...
0 комментариев