Логика по умолчанию — это немонотонная логика, предложенная Раймондом Рейтером для формализации рассуждений с предположениями о по умолчанию.

Логика по умолчанию может выражать такие факты, как «по умолчанию, что-то истинно»;напротив, стандартная логика может только выразить, что что-то истинно или что-то ложно.Это проблема, потому что рассуждения часто включают факты, которые истинны в большинстве случаев, но не всегда. Классический пример: «птицы обычно летают». Это правило может быть выражено в стандартной логике либо «всеми птицами летать», что несовместимо с тем, что пингвины не летают, либо «всеми птицами, которые не являются пингвинами, а не страусами и … летают», что требует всех исключения из правила, которое необходимо указать. Логика по умолчанию нацелена на формализацию правил вывода, подобных этому, без явного упоминания всех их исключений.

Синтаксис логики по умолчанию
Теория по умолчанию — это пара  , W — набор логических формул, называемых теорией фона, которые формализуют достоверные факты. D — набор правил по умолчанию, каждый из которых имеет вид:

В соответствии с этим дефолтом, если мы считаем, что Требование истинно, и каждый из  согласуется с нашими нынешними убеждениями, мы убеждены в том, что Заключение верно.

Логические формулы в W и все формулы по умолчанию первоначально предполагались логическими формулами первого порядка, но они потенциально могут быть формулами в произвольной формальной логике. Случай, когда они являются формулами в логике высказываний, является одним из наиболее изученных.

Примеры
Правило по умолчанию «птицы обычно летают» формализовано по умолчанию:

Это правило означает, что если X — птица, и можно предположить, что она летит, то мы можем заключить, что она летит. Фоновая теория, содержащая некоторые факты о птицах, такова:
,

Согласно этому стандарту по умолчанию, кондор летит, потому что предпосылка Bird (Condor) истинна, а оправдание Flies (Condor) не противоречит тому, что в настоящее время известно.Напротив, Птица (Пингвин) не разрешает заключительных мух (пингвинов): даже если предварительное условие Птицы по умолчанию (Пингвин) истинно, оправдание Мухи (Пингвин) не соответствует тому, что известно. Из этой теории фона и этого умолчания Bird (Bee) не может быть заключен, потому что правило по умолчанию позволяет вывести Flies (X) из Bird (X), но не наоборот. Вывод антецедентов правила вывода из последствий является формой объяснения последствий и является целью абдуктивного рассуждения.

Общее предположение по умолчанию состоит в том, что то, что не известно, является истинным, считается ложным. Это известно как Уступка закрытого мира и формализовано в логике по умолчанию, используя по умолчанию, как и следующий для каждого факта F.

Например, язык программирования Prolog использует своеобразное предположение по умолчанию при рассмотрении отрицания: если отрицательный атом не может быть доказан как истинный, то он считается ложным. Обратите внимание, однако, что Prolog использует так называемое отрицание как сбой: когда интерпретатор должен оценивать атом  , он пытается доказать, что F истинно и заключить, что  если это не удается. В логике по умолчанию вместо этого используется значение по умолчанию,  поскольку оправдание может быть применено только в том случае, если  соответствует текущим знаниям.

ограничения
Значение по умолчанию является категоричным или необязательным, если оно не имеет необходимых условий (или, что эквивалентно, его предварительное условие является тавтологическим). Значение по умолчанию является нормальным, если оно имеет одно обоснование, эквивалентное его заключению. Значение по умолчанию является сверхъестественным, если оно является категоричным и нормальным. Значение по умолчанию является полунормальным, если все его обоснования влекут за собой его вывод.Теория по умолчанию называется категоричной, нормальной, сверхъестественной или полунормальной, если все значения по умолчанию, которые она содержит, являются категоричными, нормальными, сверхнормальными или полунормальными соответственно.

Семантика логики по умолчанию
Правило по умолчанию может быть применено к теории, если ее предварительное условие связано с теорией, и ее обоснования согласуются с теорией. Применение правила по умолчанию приводит к добавлению его следствия к теории. Другие другие правила по умолчанию могут быть применены к полученной теории. Когда теория такова, что никакое другое умолчание не может быть применено, теория называется расширением теории по умолчанию. Правила по умолчанию могут применяться в другом порядке, и это может привести к разным расширениям. Пример алмаза Nixon — это теория по умолчанию с двумя расширениями:

Поскольку Никсон является республиканцем и квакером, могут применяться оба значения по умолчанию. Однако применение первого значения по умолчанию приводит к выводу, что Никсон не пацифист, что делает второй по умолчанию неприменимым. Точно так же, применяя второе значение по умолчанию, мы получаем, что Nixon является пацифистом, поэтому первый по умолчанию не применим. Поэтому у этой конкретной теории по умолчанию есть два расширения, в которых пацифист (Никсон) является истинным, а тот, в котором пацифист (Никсон) является ложным.

Исходная семантика логики по умолчанию была основана на фиксированной точке функции.Ниже приводится эквивалентное алгоритмическое определение. Если значение по умолчанию содержит формулы со свободными переменными, считается, что оно представляет собой набор всех значений по умолчанию, полученных путем предоставления значения всем этим переменным. По умолчанию  применима к теории высказываний T, если и все теории  согласуются. Применение этого значения по умолчанию к Т приводит к теории  , Расширение может быть создано путем применения следующего алгоритма:

T=W           /* current theory */
A=0           /* set of defaults applied so far */
 
              /* apply a sequence of defaults */
while there is a default d that is not in A and is applicable to T
  add the consequence of d to T
  add d to A
 
              /* final consistency check */
if 
  for every default d in A
    T is consistent with all justifications of d
then
  output T

Этот алгоритм не является детерминированным, так как несколько альтернатив могут быть применены альтернативно к данной теории Т. В примере с алмазом Никсона применение первого значения по умолчанию приводит к теории, к которой нельзя применить второе значение по умолчанию, и наоборот. В результате генерируются два расширения: один, в котором Никсон является пацифистом, и один, в котором Никсон не пацифист.

Окончательная проверка согласованности оправданий всех примененных умолчаний подразумевает, что некоторые теории не имеют никаких расширений. В частности, это происходит, когда эта проверка не выполняется для каждой возможной последовательности применимых значений по умолчанию. Следующая теория по умолчанию не имеет расширения:

поскольку  согласуется с теорией фона, можно применить дефолт, что приводит к выводу, что  false. Однако этот результат подрывает предположение, сделанное для применения первого дефолта. Следовательно, эта теория не имеет расширений.

В обычной стандартной теории по умолчанию все значения по умолчанию являются нормальными: каждый по умолчанию имеет форму  , Нормальная теория по умолчанию гарантирована как минимум одним расширением. Более того, расширения нормальной теории по умолчанию взаимно противоречивы, т. Е. Несовместимы друг с другом.

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

скептический
формула связана с теорией по умолчанию, если она связана со всеми ее расширениями;

доверчивый
формула влечет за собой теорию по умолчанию, если по крайней мере одно из ее расширений.

Таким образом, теория примеров алмазов Никсона имеет два расширения: одно, в котором Никсон — пацифист, и тот, в котором он не пацифист. Следовательно, ни пацифист (Никсон), ни ¬Пасифист (Никсон) не скептически относятся к ним, хотя оба они заслуживают доверия. Как показывает этот пример, доверительные последствия теории по умолчанию могут быть несовместимы друг с другом.

Альтернативные правила вывода по умолчанию
Следующие альтернативные правила вывода для логики по умолчанию основаны на том же синтаксисе, что и исходная система.

Оправдано
отличается от исходного тем, что по умолчанию не применяется, если при этом множество T становится несовместимым с обоснованием применяемого значения по умолчанию;

краткий
значение по умолчанию применяется только в том случае, если его следствие не связано с T (точное определение более сложное, чем это, это только основная идея);

Условный
по умолчанию применяется только в том случае, если набор, составленный из теории фона, обоснования всех примененных значений по умолчанию и последствия всех примененных значений по умолчанию (включая этот) согласованы;

рациональный
аналогично логике ограничения по умолчанию, но следствие добавления по умолчанию не учитывается при проверке согласованности;

осторожный
используемые по умолчанию, но конфликтующие друг с другом (например, примеры алмаза Nixon) не применяются.

Обоснованные и ограниченные версии правила вывода присваивают по крайней мере расширение каждой теории по умолчанию.

Варианты логики по умолчанию
Следующие варианты логики по умолчанию отличаются от исходного как по синтаксису, так и по семантике.

Условные варианты
Утверждение представляет собой пару  состоящий из формулы и набора формул. Такая пара указывает, что p истинна, а формулы предполагалось последовательным, чтобы доказать, что p истинно. Утверждающая теория по умолчанию состоит из утвердительной теории (набора утвердительных формул), называемой теорией фона, и набором значений по умолчанию, определенных как в исходном синтаксисе.Всякий раз, когда по умолчанию применяется к утвердительной теории, в теорию добавляется пара, состоящая из ее следствия и его набора оправданий. Следующая семантика использует утвердительные теории:

Кумулятивная логика по умолчанию
Обязательство по умолчанию
Квази-стандартная логика

Слабые расширения
вместо того, чтобы проверять правильность предпосылок в теории, составленной из теории фона и последствий применяемых умолчаний, предварительные условия проверяются на достоверность в расширении, которое будет сгенерировано; другими словами, алгоритм генерации расширений начинается с угадывания теории и использования ее вместо теории фона; то, что получается из процесса генерации расширений, на самом деле является расширением только в том случае, если оно эквивалентно теории, догаданной вначале. Этот вариант логики по умолчанию в принципе связан с автоэпистемической логикой, где теория  имеет модель, в которой x истинно только потому, что, предполагая истинно, формула  поддерживает исходное предположение.

Дизъюнктивная логика по умолчанию
следствием по умолчанию является набор формул вместо одной формулы. Всякий раз, когда применяется значение по умолчанию, по крайней мере одно из его последствий определяется недетерминированно и выполняется.

Приоритеты по умолчанию
относительный приоритет по умолчанию может быть явно указан; среди значений по умолчанию, применимых к теории, может применяться только один из наиболее предпочтительных. В некоторой семантике логики по умолчанию не требуется явно указывать приоритеты; скорее, более конкретные значения по умолчанию (те, которые применимы в меньшем числе случаев) предпочтительнее более менее специфических.

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

Переводы
Теории по умолчанию могут быть переведены в теории в других логиках и наоборот. Были рассмотрены следующие условия для переводов:

Последствие сохраняющих
оригинальные и переведенные теории имеют одинаковые (пропозициональные) последствия;

Верный
это условие имеет смысл только при переходе между двумя вариантами логики по умолчанию или между логикой по умолчанию и логикой, в которой существует концепция, аналогичная расширению, например, модели в модальной логике; перевод верен, если существует отображение (обычно биекция) между расширениями (или моделями) исходной и переведенной теорий;

модульная
перевод с логики по умолчанию на другую логику является модульным, если значения по умолчанию и теория фона могут быть переведены отдельно; кроме того, добавление формул в теорию фона приводит только к добавлению новых формул к результату перевода;

Same-алфавит
оригинальные и переведенные теории построены на одном и том же алфавите;

многочлен
время выполнения перевода или размер генерируемой теории должны быть полиномиальными по размеру исходной теории.

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

классическая пропозициональная логика;
аутоэпистемическая логика;
логическая логика предложения, ограниченная полунормальными теориями;
альтернативная семантика логики по умолчанию;
очертание.

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

сложность
Известна вычислительная сложность следующих задач о логике по умолчанию:

Существование расширений
решая, имеет ли теория предложения по умолчанию по крайней мере одно расширение -полное;

Скептическое влечение
решая, скептически ли теория высказывания по умозаключению влечет за собой пропозициональную формулу  -полное;

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

Проверка расширения
решая, эквивалентна ли пропозициональная формула расширению пропозициональной теории по умолчанию  -полное;

Проверка модели
решая, является ли пропозициональная интерпретация моделью расширения пропозициональной теории по умолчанию  -полное.

Реализации
Три системы, реализующие логики по умолчанию, — DeReS, XRay и GADeL