Диссертация (Исследование и разработка системы аргументации на основе пересматриваемых рассуждений для задачи обобщения), страница 7

Данное правилобазируется на интересе p/X и на аргументе q/Y. Если имеются интерес p/X иаргумент q/Y, тогда порождается интерес ~q/YX{~p}. Если в процессевывода этот интерес подтверждается, интерес p/X также подтверждается.Проиллюстрируем данное правило примером. Пусть имеется ={A1:~p},={In1:pq}.По правилу 4 “Преобразование импликации” из интересаIn1:pqполучаем интерес In2:q/{p} и аргумент A2:p/{p}. Из интереса In2:q/{p} иаргумента A2:p/{p} по правилу 8 – "редукция" строится интерес In3: p/{p,q}, который подтверждается аргументом А1: p. На рис. 2.1б интерес In3получен с помощью правила редукции.Рис. 2.1б.

Применение правил обратного вывода.47Для эффективной работы данного правила на аргументы должны бытьналожены следующие ограничения: p должен быть атомом; q должен быть либо атомом, либо импликативной формулой.Под атомом будем понимать формулу, не содержащую логических операций.Под импликативной формулой будем понимать формулы вида p  q , где p иq любые правильно построенные формулы.Доказательство полноты и состоятельности данного набора правилпрямого и обратного вывода приведены в книге Джона Поллака [14].При рассуждениях в обратном направлении создаются новые интересы.При этом образуются связи между интересами. То есть устанавливаются связитипа “предок – потомок”.Для подтверждения интереса необходимоподтверждение всех интересов, которые он порождает.Например, для подтверждения интереса q&p нужно подтверждениеобоих “дочерних” интересов p и q.

Для иллюстрации этого утверждениярассмотрим следующую задачу аргументации: <={A1: p&q}, ={In1: q&p},ℝ={}>. Исходный интерес порождает два новых интереса In2 и In3 (см. рис.2.2) подтверждение которых обеспечивает подтверждение исходногоинтереса In1.Рис. 2.2 Подтверждение нескольких интересов48Определение 2.2.

Некоторое заключение подтверждает интерес длялогики высказываний (для логики предикатов первого порядка данноеутверждение будет дополнено в § 2.1.2), если:1) формула заключения такая же, как и в интересе;2) множество посылок аргумента является подмножеством множествапосылок интереса.Пример 2.1.2. Проиллюстрируем приведённые правила прямого иобратного вывода на примере силлогизма (рис. 2.3): <={A1: ps,A2: sq },={ In1:pq }, ℝ={}>.Рис. 2.3 Силлогизм1 шаг.Преобразуем интерес In1 с помощью правила “Преобразованиеимпликации” и получаем новый интерес In2:q / {p} и дополнительныйаргумент A3:p / {p}.2 шаг.

Применяем к аргументам A1, A3 правило “Modus Ponens” и получаемаргумент A4:s/{p}.3 шаг. Преобразуем аргументы A2, A4 с помощью правила “Modus Ponens” иполучаем аргумент A5.494 шаг. Интерес In2: q / {p} по определению 2.2 подтверждается аргументом A5.5шаг.ИнтересIn2,порождённыйинтересомIn1:pq,являетсяподтверждённым и следовательно In1 тоже подтверждается.Все интересы подтверждены, следовательно, искомая формула выводима изприведённых посылок.2.1.2 Расширение системы для поддержки логики предикатов первогопорядкаОтсутствие поддержки ЛППП значительно сужало возможностисистемы пересматриваемых рассуждений.

Наибольшее количество измененийпотребовалось внести в подсистему монотонного логического вывода.Для работы с ЛППП дополнительно вводятся следующие правилапрямого вывода [14] [44]:1) отрицание квантора существования ~( x p)  ( x) ~p;2) отрицание квантора общности ~(x p)  ( x) ~p;3) преобразование квантора общности (x) p  sb(p, x/x1), где sb(p, x/x1)– результат замены в формуле p переменной x на свободную переменную x1 суникальным именем;4) преобразование квантора существования (прямая сколемизация)( x) p  sb(p, x/(y1,y2,…,yn)), где sb(p, x/(y1,y2,…,yn) – результат замены всехвхождений x на (y1,y2,…,yn), где y1, y2,…,yn — свободные переменные в p,  сколемовская функция. Для n=0 сколемовская функция просто являетсяконстантой.Таким образом, при прямом выводе, сколемизация проводитсяаналогично тому, как это происходит при резолюции.50Однако, для правил обратного вывода все несколько сложнее.Идея заключается в том, чтобы интересы подтверждались путём ихунификации с аргументами.

Если в интересах обрабатывать кванторы такимже образом, как при прямом выводе, то будут получаться абсолютно неверныерассуждения.Проиллюстрируем это на простом примере. Предположим, что имеетсяпосылка F(a), интересы x F(x) и x F(x). Если в интересе x F(x) убратьквантор общности и заменить x на свободную переменную x1 получим интересF(x1). Этот интерес унифицируется, с аргументом F(a) и получается, чтоинтересx F(x) выводим из посылки F(a), что является в корне невернымвыводом.

И наоборот, если к интересу x F(x), применить сколемизацию,получим интерес F(sc_x), где sc_x – 0-арная сколемовская функция. ИнтересF(sc_x), не унифицируем с F(a), а это означает, что интерес x F(x) неподтверждается аргументом F(a), что также в корне неверно.Поэтому при обратном выводе необходимо использовать обратнуюсколемизацию (reverse skolemization - RSK), суть которой заключается вобратной трактовке кванторов общности и существования [14]. Это означаетприменение операции отрицания к сколемовской форме для отрицанияформулы интереса. Предположим, имеется интересD=где1,…,n1 x12x2… nxn (P(x1,…,xn),– кванторы общности или существования,тогда обратнаясколемизация (RSK) для этого интереса будет иметь следующий вид:RSK(D) = ~SK{~( 1x12 x2 … nxn) P(x1,..,xn)},где SK(p) – прямая сколемизация выражения p.

Например, обратнаясколемизация для интереса ( x)( y) F(x,y) будет следующей: RSK(x y51F(x,y))=~SK(~(xyF(x,y)))=~SK(xy~F(x,y))=~(~F(x1,sc_y(x1))=F(x1,sc_y(x1)).Возвращаясь к предыдущему примеру, из интереса x F(x) будетстроиться интерес F(x1), где x1 – свободная переменная.

Такой интерес ужебудет унифицируем с любым аргументом вида F(p), где p – схематическаяпеременная, в частности он будет унифицироваться с заданным аргументомF(a). Итак, для интересов мы меняем значения кванторов общности исуществования на обратные. Введем для этого следующие правила обратноговывода [14]:1) преобразование квантора существования sb(p, x/x1)( x) p, гдеsb(p,x/x1) – результат замены в формуле p переменной x на свободнуюпеременную x1 с уникальным именем;2) преобразование квантора общности sb(p, x/(y1,y2,…,yn)( x) p, гдеsb(p, x/(y1,y2,…,yn) – результат замены всех вхождений x на (y1,y2,…,yn), гдеy1, y2,…,yn — свободные переменные в p,  - сколемовская функция..Необходимо уточнить понятие подтверждения интереса, приведённогов § 2.1.

Для этого введем некоторые вспомогательные определения.Определение 2.3 [45] Подстановкой будем называть конечноемножество вида U={t1/x1, t2/x2…tn/xn}, где ti – терм, xi – переменная.Пусть U некоторая подстановка, W - некоторое выражение. Тогда WUбудем называть примером выражения W, полученным заменой всехвхождений переменной xi (1<i<n) на терм ti.Подстановку U будем называть унификатором для выражений W1 и W2,если W1U=W2U.Введем понятие унификатора для аргументов. Аргументы A1: p/X иA2: q/Y унифицируемы, если  U : (pU=qU)  (XU  YU  YU  XU).52Предлагается использовать механизм унификации для подтвержденияинтересоваргументами.Дляэтогомодифицируемопределение2.2следующим образом.Определение 2.2*. Некоторый аргумент подтверждает интерес, если:1) существует унификатор U, который унифицирует заключениенекоторого аргумента с заключением интереса;2) множество посылок аргумента с учётом применения к немуунификатора U является подмножеством множества посылок интереса.Подробный пример работы данного метода рассмотрен в § 4.2.1.Приведём алгоритмы, которые были предложены и программнореализованы в разработанной системе.2.2 Алгоритмы монотонного выводаПриведём основные алгоритмы, которые использовались для реализацииподсистемы монотонного вывода: алгоритм прямого вывода, алгоритмобратного вывода, а также алгоритм подтверждения интересов и унификации[14].2.2.1.

Алгоритм прямого выводаВходные данные: Множество аргументов , граф вывода G.Выходные данные: Список новых аргументов New_ arguments,изменённый граф вывода G*.Шаг 1. Для данного аргумента q проверить возможность примененияпростых правил прямого вывода, не требующих участия других аргументов(упрощение, устранение эквивалентности, устранение двойного отрицания,преобразование дизъюнкции, правила Де Моргана, отрицание импликации,правила обработки кванторов).53Шаг 2. Если хотя бы одно правило вывода подходит, сделать выводсогласно правилу, при этом посылки у заключительного аргумента будуттакими же, как и у аргумента q. Перейти к шагу 4.Шаг 3. Если не одно простое правило не подошло, и аргумент q / X имеетвид A  B / X , (где A и B – любые правильно построенные формулы), тозапустить цикл перебора по всем аргументам pi / Yi , и пробовать применитьсхемы вывода Modus Ponens и Modus Tollens. Modus Ponens: если для некоторого pi / Yi результат unificate(A / X,pi / Yi ) истинен (то есть существует унификатор U), то вывестиаргумент (U*B / U*X ) Modus Tollens: если для некоторогоpi / Yi  ~ ri / Yiрезультатunificate(B / X, ri / Yi ) истинен (то есть существует унификатор U),то вывести аргумент (U*(~B) / U*X )Шаг 4.

Если аргументы, полученные на шагах 2 и 3 не содержатся вграфе вывода G, то добавить их в выходной список новых аргументовNew_arguments. Если список аргументов New_arguments – пуст, то завершитьалгоритм. В противном случае получить новый граф вывода G* путемдобавления полученных аргументов в граф вывода G и перейти к Шагу 1.Процедура unificateВходные данные: формула f1,f2.Выходные данные: унификатор U, логическая переменная result.Шаг 1.

Установить k=0; =W={f1,f2}, = .Шаг 2. Если не является одноэлементным множеством, то перейти кшагу 3. В противном случае U= , result=true; и окончить работу.54Шаг 3. Каждая из литер в Wk рассматривается как цепочка символов, ивыделяются первые подвыражения литер, не являющихся одинаковыми у всехэлементов Wk, т.е. образуется так называемое множество рассогласований типа{x,t}. Если x – переменная, а t – терм, отличный от x, то перейти к шагу 4.