Основные понятия логики умолчаний
Теория б{Bird (Tweety) Ъ Bird (Joe)}, {: ШBird (Tweety) / ШBird (Tweety);: ШBird (Joe) / ШBird (Joe)}с имеет два расширения Th ({Bird (Tweety) & ШBird (Joe)}) и Th ({ШBird (Tweety) & Bird (Joe)}). Теория с умолчаниями — это пара бW, Dс, где W — множество формул логики предикатов первого порядка, а D — множество умолчаний. Когда к теории ДСМ-рассуждений добавляются аксиомы, возможны несколько… Читать ещё >
Основные понятия логики умолчаний (реферат, курсовая, диплом, контрольная)
Определение теорий с умолчаниями и их расширений.
Умолчание — это правило вывода вида, где A (x1,…, x n) — посылка умолчания, B1(x1,…, x n),…, B k(x1,…, x n) образуют подтверждение умолчания и С (x1,…, x n) — заключение умолчания. Будем его записывать в одну строчку: A (x1,…, x n): B1(x1,…, x n),…, B k(x1,…, x n) / С (x1,…, x n). Неформально оно означает: «Для всех индивидуумов a1,…, a n если мы допускаем A (a1,…, a n) и каждое из высказываний B1(a1,…, a n),…, B k(a1,…, a n) не противоречит допускаемому, то мы будем допускать и С (a1,…, a n)».
Теория с умолчаниями — это пара бW, Dс, где W — множество формул логики предикатов первого порядка, а D — множество умолчаний.
Для теории T = бW, Dс в языке L определим оператор Г, отображающий множество формул S Н L в наименьшее множество формул Г (S) НL, такое, что:
Г (S) = Th (Г (S));
W Н Г (S);
если [A: B1,…, B k / С]ОD, A ОГ (S) и ШB1П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 (x1,…, x n) A1(x1,…, x n),…, A m(x1,…, x n), Ш B1(x1,…, x n),…, ШB k(x1,…, x n) заменяется на A1(x1,…, x n)& …&A m(x1,…, x n): B1(x1,…, x n),…, B k(x1,…, x n) / С (x1,…, x n).
В работе [Виноградов, 1999] было показано, что для формализации правдоподобных рассуждений типа ДСМ достаточно ограничиться классом стратифицированных логических программ [Chandra, 1985].
Для таких программ существует единственная наименьшая модель — итерированная неподвижная точка, которая совпадает с единственной стабильной моделью. При переводе Гельфонда-Лифшица соответствующая теория с умолчаниями будет иметь единственное расширение.
Модификационные исчисления. Для теорий с умолчаниями имеется две теоремы, характеризующие расширения. Первая описывает расширение как предел расширяющегося множества теорем из фрагментов E j:
Множество формул E — расширение теории T = бW, Dс, если и только если E = И j E j, где E0 = W, E j+1 = Th (E j) И {C: [A: B1,…, B k / С] О D, E j|_A и ШB1 П E, …, ШB k П E}.
Вторая характеризует расширение как множество теорем из объединения начальной теории W и множества заключений, порождающих его умолчаний.
Для расширения E теории T = бW, Dс множество порождающих умолчаний — это GD (E, T) = {[A: B1,…, B k / С] ОD: A ОE, ШB1 П E, …, ШB k П E}.
Если множество формул E — расширение теории T = бW, Dс, то E = Th (W И {C: [A: B1,…, B k / С] О GD (E, T)}).
Основываясь на этих теоремах, можно разработать теорию доказательств для скептического (формула истинна во всех расширениях) и доверчивого (формула истинна в каком-нибудь расширении) отношений следования.
В своей книге [Anshakov, 2010] О. М. Аншаков и Т. Гергей разработали альтернативный подход — модификационные исчисления.
В применении к формализации ДСМ-рассуждений модификации соответствуют переходу от внутреннего истинностного значения t (фактическое незнание) к внутреннему истинностному значению +1 (фактическая истина).
Например, (+)-правило 1-го рода записывается как импликация:
Jt(VЮ2 {p})&Ma+(V,{p}) & ШMa_ (V,{p}) Й J+1(VЮ2{p}). Однако, правила: J0(VЮ2{p}) Ma+(V,{p}), Ma_(V,{p}), ШJ+1(VЮ2{p}), ШJ-1(VЮ2{p}) и J+1(VЮ2{p}) Ma+(V,{p}), ШJ0(VЮ2{p}), ШJ-1(VЮ2{p}.
переписываются как умолчания и соответствующий вывод может быть рассмотрен как модификационный.
Как показано в [Виноградов, 2001] итерированная неподвижная точка совпадает для конечных доменов с единственной моделью ДСМ-метода.
Когда к теории ДСМ-рассуждений добавляются аксиомы, возможны несколько моделей, и требуется полная мощь логики умолчаний.
Благодарности.
логика умолчание модификационный исчисление.