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

Задача по предмету «Программирование»
Информация о работе
  • Тема: Определение 8.2.17. Для упорядоченной теории Г и аргумента А
  • Количество скачиваний: 4
  • Тип: Задача
  • Предмет: Программирование
  • Количество страниц: 26
  • Язык работы: Русский язык
  • Дата загрузки: 2014-05-05 17:59:30
  • Размер файла: 188.06 кб
Помогла работа? Поделись ссылкой
Ссылка на страницу (выберите нужный вариант)
  • Определение 8.2.17. Для упорядоченной теории Г и аргумента А [Электронный ресурс]. – URL: https://www.sesiya.ru/zadacha/programmirovanie/opredelenie-8217-dlya-uporyadochennoy-teorii-g-i-argumenta-a/ (дата обращения: 25.06.2021).
  • Определение 8.2.17. Для упорядоченной теории Г и аргумента А // https://www.sesiya.ru/zadacha/programmirovanie/opredelenie-8217-dlya-uporyadochennoy-teorii-g-i-argumenta-a/.
Есть ненужная работа?

Добавь её на сайт, помоги студентам и школьникам выполнять работы самостоятельно

добавить работу
Обратиться за помощью в подготовке работы

Заполнение формы не обязывает Вас к заказу

Информация о документе

Документ предоставляется как есть, мы не несем ответственности, за правильность представленной в нём информации. Используя информацию для подготовки своей работы необходимо помнить, что текст работы может быть устаревшим, работа может не пройти проверку на заимствования.

Если Вы являетесь автором текста представленного на данной странице и не хотите чтобы он был размешён на нашем сайте напишите об этом перейдя по ссылке: «Правообладателям»

Можно ли скачать документ с работой

Да, скачать документ можно бесплатно, без регистрации перейдя по ссылке:

Определение 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 Аргумент <