Лекции 2-11. Математическая логика (до колка) (Лекции 2014), страница 17

куда-то вечером мы пойдем.Но куда же мы пойдем?Поскольку в этом выводе вместо целевой переменной X былиодновременно (параллельно) подставлены разные термы кинои парк, то все, что мы можем сказать — это X ∈ {кино, парк}.Мы сумели доказать существование требуемого предмета X , ноне сумели вычислить его конкретное значение. Такиедоказательства называются неконструктивными .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯЧтобы резолютивный вывод позволял проводить вычисления,он должен быть конструктивным .Но, как показывает пример «вечернего развлечения», не всепротиворечивые системы дизъюнктов допускаютконструктивное резолютивное опровержение.

Значит, длявычислительных целей нужно выбрать такой подкласс формуллогики предикатов, для которых резолютивное опровержениеоказывается конструктивным.Заметим, что при решении задач «любовного квадрата» и«маршрута в графе» мы построили входное резолютивноеопровержение, инициированное формулой-запросом, а прирешении задачи «вечернего развлечения» такое опровержениепостроить в принципе невозможно.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯЗначит, для того, чтобы использовать метод резолюций каксредство вычислений, нужно ограничиться входнымрезолютивным выводом. Удалось обнаружить широкий классформул, для которых резолютивное опровержение всегда имеетлинейную структуру.

Это — хорновские дизъюнкты .ОпределениеЛитера L называется положительной , если L — это атом.Литера L называется отрицательной , если L = ¬A, где A — этоатом.Дизъюнкт D = L1 ∨ L2 ∨ · · · ∨ Ln называется хорновскимдизъюнктом (horn clause ), если среди литер L1 , L2 , . . . , Lnимеется не более одной положительной литеры.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПримеры.Хорновские дизъюнкты:D10D20D30D40====¬L(Паша, Y ) ∨ ¬L(X , Y ) ∨ L(Паша, X ),¬Arc(v1 , Y1 ) ∨ ¬R(Y1 , v6 , U1 ),Arc(v6 , v4 ),¬R ∨ E (кино).А вот этот дизъюнкт — нехорновский:D 00 = R ∨ E (парк).РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯХорновский дизъюнктA0 ∨ ¬A1 ∨ ¬A2 ∨ · · · ∨ ¬Anравносилен формуле(A1 &A2 & . . .

&An ) → A0 ,которая выражает утверждение:«Если выполнены условия A1 и A2 и . . . и An , то верно A0 ».В подавляющем большинстве случаев именно в такой формемы выражаем наши позитивные знания (условные ибезусловные).РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯХорновский дизъюнкт¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cmравносилен формуле¬(C1 & C2 & . . . & Cm ),и это есть отрицание запроса Q(X1 , . . .

, Xk ) = C1 &C2 & . . . &Cm ,который выражает требование:«Найти такие значения переменных X1 , . . . , Xk , которыеудовлетворяют условиям C1 и C2 и . . . и Cm ».Большинство наших вопросов представлено именно в такойформе.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯРезолютивное опровержение систем хорновскихдизъюнктов — это вычисление ответов на простыезапросы, обращенные к базе позитивных знаний.Базы позитивных знаний (хорновские дизъюнкты)становятся, таким образом,ЛОГИЧЕСКИМИ ПРОГРАММАМИ .КОНЕЦ ЛЕКЦИИ 11..