Определение 8.2.17. Для упорядоченной теории Г и аргумента А

Определение 8.2.17. Для упорядоченной теории Г и аргумента А,
А является обоснованным относительно Г тогда и только тогда, когда A - минимальная фиксированная точка Fг.
A является аннулированным относительно Г тогда и только тогда, когда А атаковано аргументом В и В является обоснованным относительно Г.
А является защищаемым относительно Н тогда и только тогда, когда А не является ни обоснованным, ни отменённым относительно Г.
Пример 8.2.10 Рассмотрим следующие правила где r0 < r3:
r0 : => α r1: α => β r2: ~β => γ r3: => ̚ α
Некоторые аргументы из этой базы знаний включают следующие:
A0 = [r0] A1 = [r0, r1] A2 = [r2] A3 = [r3]
Отсюда мы имеем, что A0 и A1 являются аннулированными, а A2 и A3 обоснованным.
Рассмотри теперь понятие диалектической теории доказательств. Её идея состоит в том, что у нас есть два игрока, Р – сторонник, O – противник и они участвуют в диалоге. Каждый шаг в игре включает в седя предоставление аргумента. Этот процесс в результате получает дерево доказательств.
Определение 8.2.18 Шаг – это пара вида (Pi, Ai) где I > 0, Pi – это игрок (O ᴗ P) и Ai – это аргумент. Диалог – это конечная непустая последовательность ходов, которая удовлетворяет следующим условиям:
если i не чётное, то Pi это P, иначе Pi это O
если Pi = Pj = P и I ≠j, тогда Ai ≠ Aj
если Pi = P и i > 1, тогда Ai – минимальный (относительно отношения включения множеств) аргумент, строго поражающий Ai-1.
если Pi = O, тогда Ai поражает Ai-1
Определение 8.2.19 Диалоговое дерево – это конечное дерево ходов, в котором каждая ветвь является диалогом. Пусть T – это диалоговое дерево для которого не может быть добавлено ещё ходов (т.е. каждый его лист не имеем ходов, которые могут быть добавлены). Игрок побеждает на ветви T (т.е. в диалоге) если он сделал последний ход (т.е. ход в лист). Игрок побеждает в диалоговом дереве тогда и только тогда, когда он выигрался во всех ветвях T.
Определение 8.2.20 Аргумент А – это доказуемо обоснованный аргумент тогда и только тогда, когда есть диалоговое дерево с А в корне и на нём побеждает сторонник А. Строгий литерал L является доказуемым обоснованным заключением тогда и только тогда, когда это заключение на основе доказуемого обоснованного аргумента.
Пример 8.2.11 Рассмотрим следующие правила, где r4 < r1 и r3 < r6:
r1: => α r2: α => β r3: β => γ r4: => ̚ α r5: ̚ α => δ r6: δ => ̚ γ
Теперь рассмотрим следующее диалоговое дерево в котором ни один из игроков не может сделать больше ходов.

Не возможно для игрока О добавить аргумент {r4: => ̚ α} потому что аргумент не побеждает P2, так как r4 < r1. Таким образом, аргумент в корне доказуемо обоснованный аргумент, и, следовательно, это приемлемый аргумент.
Семантика и доказательство теории совпадают. Так же можно показать, что все доказуемо обоснованные аргументы являются обоснованными.
Существует расширение аргумента на основе расширенного логического программирования которое поддерживает рассуждения о приоритетах. Это означает, что привилегированные отношения могут быть зависимы от контекста, и даже могут быть предметом аргументации. Это потенциально важно при моделировании интеллектуального рассуждения в целом, и особенно важно в таких приложениях, как, к примеру, приложениях для правового обоснования.
8.2.4 Пересматриваемое логическое программирование
ПЛП – это форма логического программирования, основанная на пересматриваемых правилах [GS04]. Язык и доказательство теории включает в себя ряд идей из других предложений по пересматриваемым рассуждениям (включая LDR, пересматриваемую аргументацию со специфичными свойствами и основанное на аргументах расширенное логическое программирование), вместе с собственными разработками для расширения данных идея, которые позволяют создать формализованные жизнеспособные модели. Кроме того, имеются программные реализации средств доказания теорем.
Определение 8.2.21 Язык ПЛП – это сочетание следующих типов формул:
Факт: литерал основания
Строгое правило: Правило вида α ← β1, …, βn, где α и β1,…,βn – литералы основания
Пересматриваемое правило, правило вида α -< β1,…,βn где α и β1, …, βn – литералы основания
Программа для ПЛП – это тройка (Г, Π, Δа), где Г – это множество фактов, П – это множество строгих правил, и Δа – множество пересматриваемых правил.
Для удобства обозначения в примерах, некоторые правила будут представлены в схематическом виде с помощью переменных. Это сокращение для соответствующих правил из основания может быть получено через заземление переменных с использованием постоянных символов в языке.
Пример 8.2.12 Далее представлены факты:

Далее представлены строгие правила:

Далее представлены пересматриваемые правила:

Литерал основания получается и пересматривается из программы Π путём применения форму Modus Pones как показано в следующем определении пересматриваемого вывода.
Определение 8.2.22 Пусть (Г, Π, Δа) – программа. Пересматриваемый вывод литерала основания α из Г ᴗ Π ᴗΔа |~ α, состоит из конечной последовательности литералов основания γ1, …., γn, причём γn – это α, и для каждого k ∈{1, …, n}, литерал γk либо факт в Г ᴗ правило (строгое ᴗ пересматриваемое) в Π ᴗДелта с последовательностью γk и литералами предшествующим δ1,…,δi в последовательности γ1, …, γk-1.
Пример 8.2.13 Продолжаем рассматривать пример 8.2.12, последовательность c(t), b(t), f(t) это пересматриваемый вывод для литерала f(t) при использовании правил {b(t) ← c(t), f(t) -< b(t)}.
Определение 8.2.23 Множество фактов и правил Σ несогласны тогда и только тогда, когда для некоторого α Σ |~ α, Σ |~ ~α.
Следующее определение аргумента аналогично представленному в главе 3 (смотрите определение 3.2.1), за исключением языка, отношение следствия и понятия последовательности заменяются на соответствующие в ПЛП. В противном случае, оба определения используют минимальную последовательность формул, что проверяет утверждение аргумента.
Определение 8.2.24 Аргумент в ПЛП – это пара <F, α> такая что:
F ⊆ Δа
Г ᴗΠ ᴗF |~ α
Г ᴗΠ ᴗF не противоречиво
не существует такого F’ C Ф такого что Г ᴗΠ ᴗF’ |~ α
Пример 8.2.14 Продолжаем работать с примером 8.2.12, аргументы, которые можно из него получить, следующие:

Определение 8.2.25 Аргумент <F, α> субаргумент аргумента <F’, α’> если F ⊆ F’
Определение 8.2.26 Пусть (Г, Π, Δа) – это программа. Два литерала основания α и β противоречиво согласны тогда и только тогда, когда множество Г ᴗΠ ᴗ{α, β} противоречиво.
Определение 8.2.27 Аргумент <