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

Впротивном случае окончить работу: не унифицируемо.Шаг 4. Положить +1 = {/} и +1 = {/}Шаг 5. Установить k=k+1; перейти к шагу 2.Рассмотрим работу алгоритма на следующем примере.Пример2.2.1.Пустьзаданомножествоаргументов={A1:( x)P(x)(Q(x)&R(x)), A2:P(a)}.Шаг 1. Для аргумента A1:x (P(x)Q(x)&R(x)) подходит правилопреобразования квантора общности ( x) p sb(p, x/_x) (см.

§ 2.1.2).Шаг 2. Применить найденное на шаге 1 правило вывода. Получаем аргументА3: P(_x)Q(_x)&R(_x), где _x – свободная переменная, переходим к шагу 4.Шаг 4. Полученный новый аргумент А3 добавляется в граф вывода G ипереходим к шагу 1.Шаг 1. Для аргумента A2:P(a) простые правила вывода не подходят,переходим к шагу 3.Шаг 3. Для аргумента A2:P(a) и аргумента А3: P(_x)Q(_x)&R(_x) существуетунификатор U= {a/_x}, такой, что он унифицирует P(a) и P(_x), иследовательно применима формула Modus Ponens. Применяя правило выводасовместно с унификатором U получаем новый аргумент A4:Q(a)&R(a).Переходим к шагу 4.Шаг 4.

Полученный новый аргумент А4 добавляется в граф вывода G ипереходим к шагу 1.55Шаг 1. Для аргумента A4:Q(a)&R(a) применимо правило упрощение (p & q) {p, q}.Шаг 2. Получить из аргумента A4 два новых аргумента A5: Q(a) и A6: R(a).Шаг 4.

Полученные новые аргументы А4 добавляется в граф вывода G иосуществляется переход к шагу 1.Шаг 1. Простые правила не применимы ни к одному аргументу.Шаг 3. Modus Ponens и Modus Tollens не применимы ни к одному аргументу.Шаг 4. Новых аргументов нет, завершить алгоритм вывода.Граф вывода представлен на рис 2.4Рис 2.4. Пример работы алгоритма прямого вывода.2.2.2. Алгоритм обратного выводаВходные данные: Интерес q.Выходные данные: Список новых интересов New_interestsШаг 1. Для данного интереса q проверить возможность примененияправил обратного вывода.

Если подошла схема вывода {f1,...,fn}  q/X сдополнительной посылкой d, где f1,...,fn как и ранее посылки, а q/X –заключение, то перейти к шагу 2. В противном случае перейти к шагу 4.Шаг 2. Если d –не пустая ППФ выполнить шаг 2.1. В противном случаевыполнить шаг 3.Шаг 2.1. Добавить d/{d} в список аргументов и в очередь вывода.56Шаг 2.2.

Построить интересы {f1,...,fn} /X  {d } ,построить связимежду q и f1,...,fn,Шаг 2.3. добавить полученные интересы в очередь вывода и графвывода.Шаг 3.Если d – пустая ППФ, то построить интересы f1,...,fn / X ,построить связи между q и f1,...,fn добавить полученные интересы в очередьвывода и граф вывода.Шаг 4. Интересы, полученные на шагах 2 и 3 добавить в выходнойсписок новых интересов New_interests.

Если New_interests=, то завершитьалгоритм, в противном случае перейти к шагу 1.Рассмотрим пример применения данного алгоритма.Пример 2.2.2. Пусть имеется множество интересов = {In1: ( x)R(x))}.Шаг 1.Для интереса In1: (x R(x)) применимо правило преобразованияквантора существования sb(p,x/x1)( x)p, где sb(p, x/_x) – результат заменыв формуле p переменной x на свободную переменную _x с уникальнымименем. Перейти к шагу 2.Шаг 2.

Множество дополнительных посылок d пусто, следовательно,переходим к шагу 3.Шаг 3. Построить новый интерес In2: R(_x). Добавить In2 в граф вывода G иперейти к шагу 4.Шаг 4. Добавить полученный интерес в список новых интересов. Перейти кшагу 1.Шаг 1. Ни одно из правил обратного вывода не подошло, переходим к шагу4.Шаг 4. Список новых интересов пуст. Завершить алгоритм.57Пример будет продолжен после рассмотрения алгоритма подтвержденияинтересов. Граф вывода приведён на рис. 2.5.Рис.

2.5 Обратный вывод2.2.3. Алгоритм подтверждения интересовВходные данные: Список аргументов .Выходные данные: Очередь вывода, граф вывода.Шаг 1. Для каждого неподтверждённого интереса Ini: pi / X i и аргументаAj=qj/Yj выполнить u=unificate(pi, qj).Шаг 2. Для тех интересов Ini, которые унифицируются унификатором Uс аргументом qj/Yj, проверить вложен ли результат применения унификатораU(Yj) в U( X i ).

Если вложен, то построить новый интерес Ink+1: piU / XiU, гдеk - количество интересов в графе вывода. Пометить новый интерес, какдоказанный, добавить его в граф вывода, добавить в очередь вывода.Рекурсивно пометить как доказанные интересы (и применить к нимунификатор U), которые порождают данный интерес, если они порождалитолько один интерес или все другие порождённые ими интересы ужеподтверждены.Вернёмся к примеру 2.2.2. Добавим к имеющемуся множеству интересовмножество аргументов = {A1: R(a)}.58Шаг 1.

Интерес In2: R(_x) является неподтверждённым и унифицируется саргументом A1: R(a) с помощью унификатора U={a/_x}. Перейти к шагу 2.Шаг 2. Построить интерес In3: R(a), который подтверждается аргументом A1.Подтверждённый интерес In3 рекурсивно подтверждает интерес In2, которыйего породил. Интерес In2 в свою очередь подтверждает исходный интерес In1.Граф вывода для данного примера приведён на рис 2.6.Рис. 2.6. Подтверждение интересов.Более подробный пример применения алгоритмов монотонного выводаприведён в § 4.4.1.2.3Методыпересматриваемоговывода.Обоснованиеипоражение аргументовНа каждом шаге работы системы определение статусов каждогоаргумента (поражается ли он или нет) играет ключевую роль. Определениестатусов поражения осложняется, тем, что необходимо учитывать такиесложныеслучаикакмножественныйконфликтпересматриваемыхаргументов, самопоражение и поражение собственного базиса.59Аргумент называется начальным, если множество его родителей пусто,то есть он задан изначально.

Базисом аргумента будем называть множествоаргументов, использовавшихся при его выводе.Функция σ назначает временный статус аргументам, дающая значения“поражённый” или “непоражённый” подмножеству узлов графа вывода такимобразом, что [13], [46]: σ присваивает статус “непоражённый” всем начальным узлам. σ присваивает статус “непоражённый” узлу n тогда и только тогда,когда σ присваивает статус “непоражённый” всем узлам из базисаузла n и σ присваивает статус “поражённый” всем узлам,поражающим узел n. σ присваивает статус “поражённый” узлу n тогда и только тогда,когда либо некоторым узлам из базиса n присвоен статус“поражённый”, либо некоторым поражающим узел n узламприсвоенстатус“непоражённый”. σ назначает окончательный статус аргумента n, если σ назначаетвременный статус и σ не участвует в назначении статусов другимаргументам, связанным c n.Узел является непоражённым, если все σ назначают ему статус“непоражённый”, иначе он поражённый.Заключение обосновано в данный момент рассуждений тогда и толькотогда, когда его поддерживают непоражённые аргументы.

Однако дальнейшиерассуждения могут выявить еще какие-либо значимые аргументы, которыеменяют статус заключения на необоснованное или наоборот. При наличииряда посылок и массива выводов и правил вывода можно сказать, чтовысказывание подтвержденотогда и только тогда, когда граф вывода,60построенныйнепоражённыйнамножествеузел,всехвозможныхсоответствующийаргументов,заключению.содержитПодтверждённыевысказывания являются “окончательно обоснованными” заключениями,которые система и стремится определить.2.3.1 Множественное поражениеПример множественного поражения изображен на рисунке 2.7.Возникает вопрос, какие статусы должны быть присвоены таким узлам.Рис.

2.7 Множественный конфликт пересматриваемых аргументовВведём обозначение X – такое подмножество аргументов, что каждыйэлемент которого поражается другим элементом из X, при этом ни одинэлемент X не поражается ни одним аргументом не из X.Очевидно, что неправильно считать элементы X непоражёнными.Однако считать их всех полностью поражёнными тоже неправильно.Поэтому следует различать два вида поражённых узлов. Узелпоражается “полностью” другим узлом, который является непоражённым.Такие узлы на графе вывода будем помечать тёмно-серым. В этом случае, еслипоражённый узел поражает какой-либо другой узел, то этот узел остаетсянепоражённым. Но узел может быть поражён “множественно”.

То есть два иболее непоражённых узла поражают друг друга. После чего они всеоказываются поражёнными. Но если один из них поражает еще какой-либо61узел, то этот другой узел тоже будет считаться поражённым, несмотря на то,что его поражает поражённый узел.Поражённые узлы, которые могут поражать другие узлы, являются“временно” поражёнными. Без дополнительной информации такие конфликтысчитаются неразрешимыми. На графе вывода будем обозначать такие узлысерым цветом с двойным пунктирным овалом.Подтверждённые узлы на графе вывода будем помечать светло-серымцветом с двойным сплошным овалом, поражённые – тёмно-серым, с белымибуквами.2.3.2 СамопоражениеДругим особым случаем является случай самопоражения.Определение 2.4.