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

Граф вывода – граф, показывающий взаимосвязи междуаргументами и интересами. Он отображает, из каких аргументов порождаетсяновый аргумент. Аналогично в нём показывается, из каких интересовполучаются новые интересы. Кроме того, граф вывода отображает конфликтымежду аргументами. На всех иллюстрациях будем обозначать аргументыовалами, интересы прямоугольниками.Кроме аргументов и интересов в системе аргументации предусматриваетсявозможность задания правил вывода. Разрабатываемая система обладаетнабором встроенных правил вывода, таких как Modus Ponens, Modus Tollens,контрпозиция и некоторых других.

Подробнее, встроенные правила выводабудут рассмотрены в § 2.1. Кроме встроенных правил вывода, пользовательможет задавать правила вывода следующих типов: дедуктивное следствие,пересматриваемое следствие и подрывающее следствие.Определение 1.5.6.Дедуктивные следствия– простые,дедуктивныеправила вывода, означающие, что если истинно P, то истинно и Q. Такиеправила не являются пересматриваемыми. Записывать такие правила будем36так: . На графе вывода будем отображать их обыкновенными стрелками(см. аргументы P и Q на рис. 1.6a).Определение 1.5.7. Пересматриваемые следствия - пересматриваемыеправила вывода, которые могут быть получены, например,в результатеиндукции или абдукции. В данной работе нас не интересует конкретныймеханизм получения таких выводов, поэтому такие правила подаются вместес начальными аргументами на вход программы.

Аргументы, полученные врезультате таких выводов, будем называть пересматриваемыми. Записыватьтакие правила будем так: | На графе вывода такие связи будемотображать пунктирными стрелками, а пересматриваемые аргументы –двойным овалом и светло-серым цветом. (см. аргументы M и N на рис. 1.6б).Определение 1.5.8. Подрывающие следствия. Это аргументы, поражающиесвязь между двумя другими аргументами, соединенными пересматриваемымследствием. Например, имеется аргумент F, подрывающий пересматриваемуюсвязь | между аргументами C и D.

Такие правила подрыва будемзаписывать в виде ( @ ). На графе вывода подрывающие аргументы ипоражённые ими аргументы будем соединять жирной пунктирной стрелкой.Поражённые аргументы будем помечать тёмно-серым цветом (см. аргумент Dна рис. 1.6в).а)б)в)Рис. 1.6. Граф вывода37Приведённые выше следствия будем далее называть правилами выводав аргументационной системе и обозначать как Ri.

Множество всех правилвывода будем обозначать ℝ.Cистема аргументации получает на вход множество аргументов ,множество интересов и множество правил вывода ℝ. Задачей аргументациибудем называть кортеж <,,ℝ>. Обратим внимание, что множества ,,ℝмогут быть пустыми. В случае, когда и ℝ – пустые множества, требуетсядоказать, что интересы являются общезначимыми формулами; пустоемножество интересов может интерпретироваться как задача поискавозможных гипотез. Пустое множество ℝ означает, что в задаче отсутствуютпересматриваемыеследствия,изадачасводитсякобыкновенномудедуктивному выводу.Приведём пример задачи аргументации:={A1:D};={In1:q};ℝ={R1: (D ~q&p&s); R2: p|q; R3: s(p@q) }.В данном примере имеется один аргумент A1:D, один интерес In1:q и триправила вывода – дедуктивное следствие R1: D~q&(p&s), пересматриваемоеследствие R2: p|q и подрывающее правило R3: s (p@q).Граф вывода для данной задачи представлен на рис.

1.7.38Рис 1.7. Иллюстрация различных конфликтовНа рис. 1.7 показано поражение аргумента q. Анализ графа вывода иприсвоение статусов поражения является главной процедурой в системахаргументации. Способы назначения статусов поражения будут подробнорассмотрены в § 2.3.Восновусистемыпересматриваемыхрассужденийзаложеныследующие фундаментальные идеи [35]:1) имеет место общий критерий адекватности для автоматизированныхсистем пересматриваемой аргументации;2) проведение рассуждений, основанных на “системе флажков”;3) проведение пересматриваемых рассуждений, основанных на теорииаргументации.

Анализ статусов поражения аргументов. Алгоритм для ихопределения;4) аппарат монотонного вывода.39Остановимся коротко на первом пункте. Пунктам 2, 3 и 4 будут посвященыотдельные разделы данной работы (см. § 2.1 и § 2.3).1.5.1. Общий критерий адекватности для систем пересматриваемойаргументацииВозможно, самой большой проблемой, с которой сталкиваютсяразработчики систем автоматизированной пересматриваемой аргументации,является тот факт, что множество аргументов, полученное из исходныхаргументов, в общем случае, не является конечным.

Поэтому встаёт вопрос обадекватности такой системы, а именно насколько достоверны выводы,полученные в системе пересматриваемых рассуждений.Д. Поллак утверждает [13], что множество заключений, выдвинутоесистемой пересматриваемых рассуждений, аппроксимирует множествоподтверждённых высказываний, если выполняются следующие условия нарассматриваемые высказывания р: если р является подтверждённым, то система в итоге достигнеттого момента, когда р станет обоснованным и будет оставатьсяобоснованным в дальнейших рассуждениях; если р является неподтверждённым, то система в итоге достигнеттого момента, когда р станет необоснованным и будет оставатьсянеобоснованным в дальнейших рассужденияхТаким образом, если эти условия выполняются, то такая система рассужденийявляется адекватной по Поллаку.1.6 Выводы по главе 1.1.

В данной главе были приведены основные определения и понятиятеории аргументации, рассмотрены свойства отношения атаки, критерииприемлемости аргументов.402. Также рассмотрены основные типы аргументационных систем:абстрактные системы, системы, основанные на многозначной логике,системы, основанные на пересматриваемых рассуждениях.3.

Для практической реализации выбрана аргументация на основепересматриваемых рассуждений, так как она обладает рядом очевидныхпреимуществ: cохраняется семантика задачи; существует механизм вывода новых аргументов из уже имеющихся; основывается на простом языке формальной логики, что существенноупрощает работу системы; является немонотонной системой, что позволяет динамическидобавлять новую информацию в базу знаний.Выявлены следующие проблемы и задачи, которые необходимо решитьдля реализации системы аргументации на основе пересматриваемыхрассуждений: реализовать систему монотонного вывода с поддержкой ЛППП;разработать алгоритмы пересматриваемого вывода для ЛППП, а именноалгоритм применения правил пересматриваемого вывода и алгоритмнахожденияконфликтов;определитьметодколичественнойоценкидостоверности аргументов.41ГЛАВА 2.

МЕТОДЫ И АЛГОРИТМЫ АРГУМЕНТАЦИИ НАОСНОВЕ ПЕРЕСМАТРИВАЕМЫХ РАССУЖДЕНИЙВданнойглаверассматриваютсяосновныеметоды,которыеиспользовались при реализации системы аргументации, основанной напересматриваемых рассуждениях.пересматриваемоговывода,Приводятся алгоритмы монотонного иалгоритмынахожденияконфликтовипротиворечий.

Кроме того, будет предложено расширение системы дляподдержки предикатов первого порядка, а также будет рассмотрен механизмстепеней обоснования для нахождения числовой оценки достоверностиаргументов.2.1. Методы монотонного вывода в системах аргументацииВотличиеотсистемабстрактнойаргументации,системыпересматриваемых рассуждений предполагают наличие механизма полученияновых знаний на основе имеющейся в системе информации.

К такиммеханизмам относятся, например, методы порождения гипотез, индуктивныйи дедуктивный выводы. Классическим для систем аргументации на основепересматриваемых рассуждений является применение методов монотонноговывода.В данной работе будет рассмотрен и реализован механизммонотонного вывода на основе теории натуральной дедукции [14], [42], [43],которая является одним из методов автоматического доказательства теорем.Натуральная дедукция относится к прямым двунаправленным методампоиска. Для единообразия описания в данном разделе будем использоватьтерминологию аргументации, а именно называть выводимые формулыаргументами, а формулы, общезначимость которых требуется доказать –интересами.42Система работает с двумя списками – списком аргументов, и спискоминтересов. Изначально список аргументов состоит из посылок, а списокинтересов состоит из выражений, которые мы хотим вывести.Далее происходит двунаправленный поиск.

В одном направлениипроисходит порождение новых аргументов на основе уже имеющихся. Такойпоиск будем называть прямым. В другом направлении из множества интересовпорождаются новые интересы. Такой поиск будем называть обратным.Полученные с помощью правил вывода аргументы и интересы помещаются вочередь вывода.Определение 2.1. Под очередью вывода будем понимать очередь,состоящую из еще непроанализированных аргументов и интересов.

Всеполученные аргументы и новые интересы также помещаются в очередьвывода. Пока очередь не окажется пустой, система продолжает работать.Рассмотрим систему монотонного вывода для логики высказываний.Расширение для поддержки логики предикатов первого порядка будетприведено в § 2.1.2.2.1.1. Система монотонного вывода для логики высказыванийКак говорилось ранее, натуральная дедукция предполагает вести выводв двух направлениях от аргументов к аргументам, и от интересов к новыминтересам. На каждом шаге работы системы происходит выбор очередногоэлемента из очереди необработанных аргументов.Остановимся подробнее на каждом направлении поиска решения.Правила прямого выводаПравила прямого вывода будем записывать в следующем виде:{f1,…,fn}f,43где fi - формулы посылки, содержащие схематические переменные,f - заключение.Под схематическими переменными будем понимать любую правильнопостроенную формулу.

Так, например, правило Modus Ponens будет записанов следующем виде: {p,(pq)}q. Данное правило означает, что если естьаргументы A1:p и A2: pq, то вывести аргумент A3:q, где p и q – схематическиепеременные.В реализуемой системе натуральной дедукции будем использоватьследующий набор правил вывода, предложенный Джоном Л. Поллаком [14].1) Упрощение(p & q)  {p, q}, где {p, q} – множество из двух аргументов p и q2) Устранение эквивалентности(p=q)  (p  q) & (q  p)3) Устранение двойного отрицания~~pp4) Modus Ponens{p,(pq)}q5) Modus Tollens{~q,(pq)}~p6) Преобразование дизъюнкции(p  q)  (~p  q)7) Правила Де Моргана44¬(p & q)  (~p  ~q)¬ (p  q)  (~p & ~q)8) Отрицание импликации¬(p  q)  (p & ~q)9) Правило разъединения посылок(p & r  q)(p(rq))Рассмотрим пример применения правил прямого вывода.Пример 2.1.1. Пусть задано следующее множество аргументов = {A1:p&qd; A2: p; A3: q}.Применяя к аргументу А1 правило “разъединения посылок” получаемаргумент A4: (p (q  d)).

Далее, используя аргументы A2 и А4, по правилуModus Ponens получаем аргумент А5: (q  d). Из аргумента A3 и A5 по правилуModus Ponens получаем аргумент А6: d. На этом шаге очередь выводастановится пустой и вывод заканчивается.Граф вывода для данной задачи приведённа рис. 2.1а.Рис. 2.1а. Применение правил прямого вывода.45Правила обратного выводаПростые правила обратного вывода записываются аналогично правилампрямого вывода, например, правило Де Моргана запишется в следующемвиде:(¬p  ¬q)~(p & q).Однако обратные правила могут иметь дополнительные посылки.Например, правило q  (p  q) порождает дополнительную посылку p. Этоозначает, что если имеется интерес (p  q)/X, то строится новый аргумент p/{p}, и строится новый интерес q/X{p}. Если в дальнейшем получаетсязаключение q/Y, где YX{p}, то система сделает вывод о подтверждении(см.

опр. 2.2.) интереса (pq)/X.В реализуемой системе натуральной дедукции будем использоватьследующий набор правил обратноговывода, предложенный Джоном Л.Поллаком [14].1) Упрощение{p, q}(p & q)2) Устранение эквивалентности(pq) & (qp)  (p = q)3) Устранение двойного отрицанияp¬¬p4) Преобразование импликацииq  (p  q), с дополнительной посылкой p.5) Преобразование дизъюнкции(¬p  q)  (p  q)6) Правила Де Моргана(~p  ~q)  ¬(p & q)46{~p, ~q}  ¬(p  q)7) Отрицание импликации{p, ~q}  ¬(p  q)8) Редукция{~q}  {p},{q} с дополнительной посылкой ~pОстановимся подробнее на правиле “редукция”.