ПОИСК Статьи Рисунки Таблицы Процедуры логического вывода на основе принципа резолюции из "Экспертные системы в химической технологии" Из практических соображений удобнее использовать доказательство от противного, т. е. доказывать невыполнимость формулы. На доказательстве от противного основан метод резолюции. [c.149] В исчислении предикатов существует много различных ПВ. Обладая для ИП универсальной истинностью, они могут применяться либо для установления истинности утверждения в целом, либо для порождения заключения. Кроме того, ПВ можно использовать как отдельно, так и в сочетании с другими ПВ. Приведем некоторые основные ПВ модус поненс , модус толленс , двойного отрицания , введения конъюнкции , приведения к абсурду и специализации [16]. [c.149] Это правило используют в методе резолюций. [c.150] При реализации процедур формального вывода используют прямой и обратный методы рассуждений [9, 16, 49]. [c.150] Прямой метод (от посылок) из посылок /4- В выводит заключение В (правило модус поненс ). Основной недостаток прямого метода рассуждения состоит в его ненаправленности повторные применения метода обычно приводят к резкому росту промежуточных заключений, не связанных с целевым заключением. [c.150] Обратный метод (от цели) является направленным из желаемого заключения В и тех же посылок он выводит новое подцелевое заключение А. Каждый шаг вывода в этом случае всегда связан с первоначально поставленной целью. [c.150] Для решения одной и той же задачи можно использовать различные ПВ, а также прямой и обратный методы рассуждений. [c.150] Рассмотрим процедуры вывода решения для некоторой исходной НФЗ, постановка которой имеет следуюш,ий вид. [c.151] На языке ИП указанная задача формулируется следующим образом. [c.151] На втором шаге используют новый факт (5.18), а также правило ПО, заданное в постановке задачи (5.12), и ПВ модус толленс (5.6) для вывода требуемого заключения (5.14). [c.151] Приведем структуру процедуры формального вывода для этой задачи. [c.152] Одно из важных свойств ИП, как отмечалось ранее, состоит в том, что существует множество путей утверждения одного и того же положения. [c.152] Для доказательства (5.19) приведем структуру другой процедуры формального вывода, использующую ПВ модус поненс (5.8). [c.152] Содержательно секвенция означает Если принять допущения (гипотезы) Ai.A , то имеет место либо В , либо В2 -1Либо В . [c.152] Секвенцию 5 называют общезначимой, или тождественно истинной, если тождественно истинен ее формульный образ. [c.153] В узком смысле секвенция — это правило логического перехода А= В, которое интерпретируется следующим образом Если А истинно, то В также истинно если А ложно, то о В сказать ничего нельзя . В широком смысле понятие секвенции совпадает с понятием ядра ПП (см. разд. 5.4). В логическом исчислении /С-вы-водимыми объектами являются также секвенции. [c.153] Имеется единственная схема аксиом А А н ряд ПВ, записываемых с помощью горизонтальной черты с одной или двумя секвенциями (точнее —секвенциальными схемами) над ней, которые называются посылками ПВ, и с одной секвенциальной схемой под чертой, называемой заключением ПВ. Правила вывода делят на структурные (не содержащие логических связок) и логические [49]. [c.153] Процедура формального вывода в ис- Нксиома числении ЪК может быть отображена в виде дерева вывода, представляющего собой разновидность ДВР (рис. [c.153] Необходимо подчеркнуть, что в исчислении предикатов процедура вывода является монотонной [16, 49]. Монотонность при выводе — свойство, характерное для вывода в замкнутой формальной системе (ФС) в закрытой БЗ, состоящее в том, что ранее выведенные утверждения (ППФ) не теряют истинности при расширении множества аксиом или посылок для вывода. [c.154] Вернуться к основной статье