Cтраница 2
Если вместо семантики обобщенных устойчивых моделей для абдуктивной структуры использовать аргументационную семантику КМ-допустимости, то абдуктивная процедура доказательства становится состоятельной. [16]
Конечно, доминирующий в автоматическом доказательстве теорем метод резолюции не является панацеей от всех бед, сопровождающих процедуры доказательства теорем, и мы вправе надеяться на появление более совершенных процедур дедуктивного вывода. Это касается и языка Пролог, неплохо зарекомендовавшего себя при решении логических проблем. Здесь можно согласиться с точкой зрения Н. Н. Непейводы, утверждавшего, что есть смысл использовать Пролог для кусков программ, обладающих исключительно сложной логикой при явном задании вариантов. [17]
Таким образом, можно заключить, что процесс решения задач, требующих логических рассуждений, может быть сведен к процедуре доказательства теорем. При этом достаточно доказать либо общезначимость некоторой формулы, либо противоречивость отрицания этой формулы. В принципе это реализуется алгоритмом, который перебирает все возможные интерпретации и вычисляет для каждой из них логическое значение формулы. [18]
Конечно, не все этапы приведенных выше доказательств являются очевидными a priori, и для практической проверки типов необходимо автоматизировать процедуру доказательства в рассматриваемой системе вывода. Фактически это означает, что необходимо построить алгоритм проверки типа выражения, определяющий порядок применения правил вывода. [19]
Теорема 17.8 сводит задачу о разрешимости задачи Дирихле для вполне нелинейных эллиптических уравнений к получению серии оценок производных, обобщающих этапы I - IV из процедуры доказательства существования для квазилинейного случая, описанной в гл. Вполне нелинейная задача в общем случае значительно сложнее, так как требуется получить оценку вторых производных. В последующих разделах мы получим оценки вторых производных для различных типов уравнений, включающих примеры, рассмотренные в начале этой главы. В некоторых случаях эти оцедки не будут достаточны для прямого применения теоремы 17.7, и потому потребуются некоторые ее модификации. В частности, при рассмотрении негладкой функции F в уравнении Беллмана (17.8) используются аппроксимации. [20]
Анализ доказательства теоремы 11.5 показывает, что для эллиптических операторов вида (11.7) или (11.8) разрешимость классической задачи Дирихле с гладкими данными зависит только от выполнимости второго этапа процедуры доказательства существования, т.е. от существования оценки значений градиента на границе. [21]
Процедура доказательства основывается на семантике аргументации, сформулированной в терминах И-деревьев. Узлы в дереве - это множества целей, и каждый узел помечен как атака или защита. Термин узел обозначает или вершину дерева, или множество гипотез, связанное с этой вершиной. [22]
Будем считать, что заданы программа Р и соответствующее множество гипотез Hyp. Процедура доказательства работает непосредственно с программой Р, которая может содержать переменные. Но цель G и сгенерированное множество А не должны содержать переменных. Вообще говоря, процедуру доказательства несложно модифицировать, чтобы она, дополнительно к возвращаемым множествам гипотез, в качестве решения возвращала бы подстановки для переменных, так что ограничение для G не является существенным. Узлы в промежуточных деревьях для процедуры доказательства - это цели, которые могут содержать переменные и атомы. Используемые при этом деревья называются целевыми. [23]
После того, как определена обобщенная устойчивая модель, абдук-тивное объяснение наблюдения Q в структуре Р, А, / определяется как любое подмножество А множества А такое, что М ( А) - обобщенная устойчивая модель структуры Р, А, 1 и М ( А) Q. Процедура доказательства в этом случае содержит две фазы: абдуктивную фазу, в ходе которой выполняется стандартная SLD-резолюция, генерирующая гипотезы; и фазу непротиворечивости, состоящую в проверке того, удовлетворяют ли гипотезы ограничениям целостности. Эта процедура оказывается несостоятельной. Для достижения состоятельности было предложено использовать аргументационную семантику, единым образом работающую как с ограничениями целостности, так и с NAF ( отрицанием как неуспехом) с помощью специально определенного понятия атаки. [24]
Класс встроенных MV-зависимостей был обнаружен в работах Fagin [ 1977с ] и Delobel [1978], а в работах Parker, Parsaye-Ghomi [1980], Sadiv, Walecka [1979] было показано, что для класса одних EMV-зависимостей не существует полной, конечной аксиоматизации. Процедуру доказательства вы водимости для более широкого класса зависимостей, которые определены в гл. В работах Beeri, Vardi [ 1980a, b ], а также Chandra, Lewis, Makowsky [1981] показано, что выводимость для этого класса зависимостей неразрешима. Здесь нет противоречия, поскольку процедура доказательства выводимости включает как конечные, так и бесконечные отношения. Утверждение о выводимости может иметь бесконечный контрпример и не иметь конечного. [25]
Класс встроенных MV-зависимостей был обнаружен в работах Fagin [ 1977с ] и Delobel [1978], а в работах Parker, Parsaye-Ghomi [1980], Sadiv, Waiecka [1979] было показано, что для класса одних EMV-зависимостей не существует полной, конечной аксиоматизации. Процедуру доказательства вы водимости для более широкого класса зависимостей, которые определены в гл. В работах Beeri, Vardi [ 1980a, b ], а также Chandra, Lewis, Makowsky [1981] показано, что выводимость для этого класса зависимостей неразрешима. Здесь нет противоречия, поскольку процедура доказательства выводимости включает как конечные, так и бесконечные отношения. Утверждение о выводимости может иметь бесконечный контрпример и не иметь конечного. [26]
Однако процедура доказательства не может это определить, так как резолюция на шаге aatom зацикливается. [27]
Но процедура доказательства не может это определить, так как она не может определить, что каждая из бесконечного множества атак на not р контратакуется пустым множеством. [28]
Теория аргументации может успешно применяться для организации абдуктивного вывода. Например, процедура доказательства, описанная в разд. [29]
Логика высказываний, с которой мы сейчас имеем дело, является не самой выразительной. Разные программные системы ИИ используют различные процедуры доказательства и опровержения, рассмотрим наиболее общую теорию. [30]