Логика умолчаний как альтернатива модификационных исчислений

Д.В. Виноградов (vin@viniti.ru)

Всероссийский институт научной и технической информации, Москва

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

Введение. Первоначальное изложение ДСМ-метода автоматического порождения гипотез [Финн, 1991] использовало средства многозначных логик. Очень важной оказалась идея Д.А. Бочвара [Бочвар, 1972] о разделении внутренних (фактических) и внешних (логических) истинностных значений. Связь между истинностными значениями обеспечивается (характеристическими) J_операторами Россера-Тьюкетта. При этом подходе каждая замкнутая формула получала единственное истинностное значение. В своей книге [Anshakov, 2010] О.М. Аншаков и Т. Гергей разработали альтернативный подход -- модификационные исчисления. В этом подходе вывод состоит из внешних (J_атомарных и состоящих из них) формул, однако внутренняя (не имеющая J_связки) атомарная формула может встречаться под разными J-символами. Это означает, что в процессе вывода внутреннее истинностное значение этой формулы может изменяться. Для обеспечения непротиворечивости был предложен механизм модификации вывода.

В настоящей статье мы опишем возможность замены модификационного исчисления логикой умолчаний [Reiter, 1980]. Используя связь логики умолчаний с логическими программами [Gelfond, 1990], мы обсудим формализацию правдоподобных рассуждений типа ДСМ средствами стратифицированных логических программ [Виноградов, 1999, 2001].

Основные понятия логики умолчаний

Определение теорий с умолчаниями и их расширений

Умолчание - это правило вывода вида , где A(x₁,…,x _n) - посылка умолчания, B₁(x₁,…,x _n),…, B _k(x₁,…,x _n) образуют подтверждение умолчания и С(x₁,…,x _n) - заключение умолчания. Будем его записывать в одну строчку: A(x₁,…,x _n) : B₁(x₁,…,x _n),…,B _k(x₁,…,x _n) / С(x₁,…,x _n). Неформально оно означает: «Для всех индивидуумов a₁,…,a _n если мы допускаем A(a₁,…,a _n) и каждое из высказываний B₁(a₁,…,a _n),…, B _k(a₁,…,a _n) не противоречит допускаемому, то мы будем допускать и С(a₁,…,a _n)».

Теория с умолчаниями - это пара бW, Dс, где W - множество формул логики предикатов первого порядка, а D - множество умолчаний.

Для теории T = бW, Dс в языке L определим оператор Г, отображающий множество формул S Н L в наименьшее множество формул Г(S) НL, такое, что:

Г(S) = Th(Г(S));

W Н Г(S);

если [A : B₁,…,B _k / С]ОD, A ОГ(S) и ШB₁ПS, …, ШB _k ПS, то C ОГ(S).

Множество формул E назовем расширением теории T = бW, Dс, если и только если E = Г(E).

Нормальное умолчание - это умолчание вида A:C/С. Теория T = бW, Dс называется нормальной, если все ее умолчания нормальны.

Примеры теорий с умолчаниями

Теория б{Bird(Tweety)}, {Bird(Tweety): Flies(Tweety)/ Flies(Tweety)}с имеет единственное расширение Th({Bird(Tweety) & Flies(Tweety)}).

Теория б{Bird(Tweety) Ъ Bird(Joe)}, {: ШBird(Tweety) / ШBird(Tweety); : ШBird(Joe) / ШBird(Joe)}с имеет два расширения Th({Bird(Tweety) & ШBird(Joe)}) и Th({ШBird(Tweety) & Bird(Joe)}).

Теория бЖ, { : Bird(Tweety) / ШBird(Tweety)}с не имеет расширений.

Свойства теорий с умолчаниями

Теория T = бW, Dс имеет противоречивое расширение, если и только если противоречиво W.

Если E и F - расширения теории T = бW, Dс и E Н F, то E=F.

Если у теории T = бW, Dс есть противоречивое расширение, то оно единственное.

Если W непротиворечиво, то нормальная теория T = бW, Dс имеет непротиворечивое расширение.

Если нормальная теория T = бW, Dс имеет различные расширения E и F, то EИF противоречиво.

Связь с логическими программами

В работе [Gelfond, 1990] М.Г. Гельфонд и В.А. Лифшиц связали с каждой логической программой такую теорию с умолчаниями, чтобы стабильные модели программы совпадали с расширениями теории с умолчаниями.

Перевод очень прост: каждое правило

C(x₁,…,x _n) ¬ A₁(x₁,…,x _n),…,A _m(x₁,…,x _n),Ш B₁(x₁,…,x _n),…,ШB _k(x₁,…,x _n) заменяется на A₁(x₁,…,x _n)& …&A _m(x₁,…,x _n) : B₁(x₁,…,x _n),…,B _k(x₁,…,x _n) / С(x₁,…,x _n).

В работе [Виноградов, 1999] было показано, что для формализации правдоподобных рассуждений типа ДСМ достаточно ограничиться классом стратифицированных логических программ [Chandra, 1985].

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

Модификационные исчисления. Для теорий с умолчаниями имеется две теоремы, характеризующие расширения. Первая описывает расширение как предел расширяющегося множества теорем из фрагментов E j:

Множество формул E - расширение теории T = бW, Dс, если и только если E = И _j E _j, где E₀ = W, E _j+1 = Th(E _j) И {C: [A : B₁,…,B _k / С] О D, E _j|_A и ШB₁ П E, …, ШB _k П E}.

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

Для расширения E теории T = бW, Dс множество порождающих умолчаний - это GD(E,T) = {[A : B₁,…,B _k / С] ОD : A ОE, ШB₁ П E, …, ШB _k П E}.

Если множество формул E - расширение теории T = бW, Dс, то E = Th(W И {C: [A : B₁,…,B _k / С] О GD(E,T)}).

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

В своей книге [Anshakov, 2010] О.М. Аншаков и Т. Гергей разработали альтернативный подход -- модификационные исчисления.

В применении к формализации ДСМ-рассуждений модификации соответствуют переходу от внутреннего истинностного значения t (фактическое незнание) к внутреннему истинностному значению +1 (фактическая истина).

Например, (+)-правило 1-го рода записывается как импликация:

J_t(VЮ₂ {p})&M_a⁺(V,{p}) & ШM_a^_ (V,{p}) Й J₊₁(VЮ₂{p}). Однако, правила: J₀(VЮ₂{p}) ¬ M_a⁺(V,{p}), M_a^_(V,{p}), ШJ₊₁(VЮ₂{p}), ШJ_-1(VЮ₂{p}) и J₊₁(VЮ₂{p}) ¬ M_a⁺(V,{p}), ШJ₀(VЮ₂{p}), ШJ_-1(VЮ₂{p}

переписываются как умолчания и соответствующий вывод может быть рассмотрен как модификационный.

Как показано в [Виноградов, 2001] итерированная неподвижная точка совпадает для конечных доменов с единственной моделью ДСМ-метода.

Когда к теории ДСМ-рассуждений добавляются аксиомы, возможны несколько моделей, и требуется полная мощь логики умолчаний.

Благодарности. Работа выполнена при поддержке программы фундаментальных исследований Президиума РАН «Математическое моделирование и интеллектуальные системы» на 2010 год.