Досрочный экзамен по математической логике 25 декабря 2004 года

время на выполнение работы: 2,5 часа

Условия задач:

NB: в Oper'е замечена проблема с шрифтом Symbol

1. Текст – это конечный список слов. Слово – это конечный список литер. Написать программу, ищущую самое короткое слово Х из самых часто встречающихся в тексте L слов. Запрос ? G(L, X)

2. Выразить на языке логики предикатов следующее утверждение в виде замкнутой формулы: "Если почти все элементы последовательности действительных чисел y равны между собой, то и предел последовательности равен этому же числу".

   • доступные константы:

     • 0 – константа 0

   • доступные функциональные символы

     • |x| - абсолютное значение х

     • (-х) - смена знака х

     • x+y, x-y, x*y, x/y - арифметические операции

   • доступные предикаты:

     • R(x) - вещественное число

     • N(x) - натуральное число

     • S(y) - y - последовательность действительных чисел

     • E(x,n,y) - x - элемент y с номером n

     • L(p,y) - p - предел последовательности y

     • x < y, x > y, x = y – сравнение и равенство

3. С помощью метода семантических таблиц исследовать общезначимость данной формулы:
   ($y ¬P(x) → $x R(x)) → ("x $y (¬P(x) → R(y)))

4. С помощью метода резолюций исследовать общезначимость данной формулы:
   ($y ¬P(x) → $x R(x)) → ("x $y (¬P(x) → R(y)))

5. Изобразить дерево SLD-резолютивных вычислений и дать все вычислимые ответы для следующей программы:

   ? P(x), R(x)             P(b) ← ;             P(f(b)) ← R(b), !;             P(c) ← ;             R(f(x)) ← P(x);             R(x) ← P(x);

    

6. Дать определение противоречивого множества замкнутых формул

7. Дать определение SLD-резолютивного опровержения

8. Дать определение эрбрановской интепретации формулы j

9. Операционная семантика оператора not в логическом программировании

10. Таблица áГ; Dñ состоит из замкнутых формул и не имеет успешных вычислений. Какие утверждения верны всегда и почему?

    1. Г имеет хотя бы одну модель

    2. D имеет хотя бы одну модель

    3. ни одна из ψÎD не является общезначимой

    4. ни одно из утверждений a-c не верно

     

11. Пусть S – множество дизъюнктов. Пусть S' – множество всех резольвент, получаемых из S. Какие из следующих утверждений несправедливы и почему?

    1. если S – непротиворечивое множество, то S' – непротиворечивое множество

    2. если S – противоречивое множество, то S' – противоречивое множество

    3. если S' – непротиворечивое множество, то S – непротиворечивое множество

    4. если S’ – противоречивое множество, то S – противоречивое множество

    5. среди a-d есть неверное утверждение, но его номер зависит от S

     

12. Пусть I – эрбрановская интерпретация логической программы П такая, что T_П(I) Ç I = T_П(I) ¹ I (T_П - оператор непосредственного следования). Какие из следующих утверждений верны независимо от I и П и почему?

    1. Succ_П Í I

    2. Succ_П Ì I

    3. Succ_П = I

    4. Succ_П É I

    5. Succ_П Ê I

    6. ни одно из a-e неверно в общем случае

     

Ответы:

1. программа, работающая на PDC-PROLOG

   пример оформления этой задачи

   domains     word = char*     text = word* predicates     G(text, word)     is_most_often(text, word)     exists_more_often(text, word)     occur(text, word, integer)     elem(text, word)     length(word, integer)     exists_more_short(text, word) clauses     G(L, X) :-         elem(L, X),         is_most_often(L, X),         not(exists_more_short(L, X)), !.         is_most_often(L, X) :-             not(exists_more_often(L, X)).         exists_more_often(L, X) :-             elem(L, Y),             not(Y = X),             occur(L, X, K),             occur(L, Y, K1),             K1 > K, !.         elem([X|_], X).         elem([_|L], X) :- elem(L, X).         occur([], _, 0).         occur([X|L], X, K1) :-             !, occur(L, X, K),             K1 = K+1.         occur([_|L], X, K1) :- occur(L, X, K1).         exists_more_short(L, X) :-             elem(L, Y),             is_most_often(L, Y),             length(X, LX),             length(Y, LY),             LX > LY.         length([], 0).         length([_|L], K1) :-             length(L, K), K1 = K+1.

   G(L, X) ←         elem(L, x),         is_most_often(L, x),         not(exists_more_short(L, x)),         !; is_most_often(L, x) ←         not(exists_more_often(L, x)); exists_more_often(L, x) ←         elem(L, y),         not(y = x),         occur(L, x, k),         occur(L, y, k1),         k1 > k, !; occur(nil, x, 0) ← ; occur(x.L, x, k1) ←         !, occur(L, x, k),         k1 is k+1; occur(y.L, x, k1) ←         occur(L, x, k1); exists_more_short(L, x) ←         elem(L, y),         is_most_often(L, y),         length(x, Lx),         length(y, Ly),         Lx > Ly; length(nil, 0) ← ; length(y.L, k1) ←        length(L, k),        k1 is k+1;

    

2. "y ( S(y) →
       "l ( R(l) →
               (
                   ( $n ( N(n) &
                               "m ( N(m) & m > n →
                                           $x ( R(x) & E(x, m, y) & l = x )
                               )
                   )
                  →
                   $lim ( R(lim) & L(lim, y) & l = lim )
               )
           )
       )
    
3. общезначима
    
4. общезначима
    
5. {x / b}, {x / f(b)}
    
6. - 9. - см. лекции
    
10. ответ: a, c
    1. верно, т.к. иначе бы по определению выполнимости таблицы таблица имела успешный вывод
    2. неверно. контпример: < | P(a) & ¬P(a) >
    3. верно, т.к. иначе бы таблица по теореме Геделя имела успешный вывод
    4. неверно, т.к. верно а
11. ответ: b, c, e
    1. всегда верно по лемме о резолюции к теореме о корректности метода резолюций
    2. несправедливо: контпример = { P(x) \/ P(y), ¬P(x) \/ ¬P(y) }
    3. несправедливо, см. контпример пункта b
    4. всегда верно по лемме о резолюции к теореме о корректности метода резолюций
    5. несправедливо: контрпример = { P, ¬P }
12. ответ: a, b
    2. верно,
           т.к. I É T_П(I) => I ÊT_П(I) => T_П(I)Ê T_П(T_П(I)) = T_П²(I) => I É T_П(I) Ê T_П²(I) Ê T_П³(I) Ê ... . Есть 2 варианта завершения:
       • цепочка сойдется. Тогда мы придем к lfp_П = Succ_П, поскольку наименьшая неподвижная точка единственна. Но тогда смотрим начало и конец цепочки: I É Succ_П, что доказывает начальное утверждение.
       • цепочка будет уменьшаться до Æ. Но что с ней произойдет потом? Пусть мы получили пустое множество на шаге k, т.е. T_П^k(I) = Æ, но T_П^k(I) Ê T_П^k+1(I), т.е. Æ Ê T_П(Æ), но для любого ОНС верно и то, что Æ Í T_П(Æ) (пустое множество вложено в любое множество). Т.е. Æ = T_П(Æ). Т.е. если цепочка дошла до пустого множества, то и наименьшая неподвижная точка равна пустому множеству (она же единственна). Но тогда I É T_П(I) Ê Æ = lfp_П = Succ_П, т.е. I É Succ_П, что также доказывает начальное утверждение
    1. верно, т.к. верно b
    3. неверно, т.к. при этом I = Succ_П = lfp_П => I = T_П(I) по определению неподвижной точки. Но I É T_П(I) по условию. Противоречие.
    4. неверно, т.к. при этом I Ì Succ_П = lfp_П => Succ_П не является наименьшей неподвижной точкой (есть вложенная интерпретация). Противоречие.
    5. неверно, т.к. неверны c и d
    6. неверно, т.к. верно b
        

NB: мне больше всего понравилась последняя задача (на самом экзамене я до такого доказательства пункта b даже и не догадался), тем что она красивая (не надо ломать голову над контрпримерами, а надо просто хорошо знать все формулировки теорем и определения). Прекрасно, что для решения 10-12 задач действительно достаточно их знать и здраво и логично рассуждать (я на экзамене забыл про единственность lfp, поэтому, наверное, и не придумал доказательства пункта b 12й задачи, ведь оно главным образом использует эту единственность). Иногда, конечно, приходится придумывать контрпримеры, но бывает полезно взять контпример из лекций: контрпример к пункту b 11й задачи прямо был упомянут Захаровым ("склейка важна").
Мы писали экзамен 2,5 часа - и этого как раз вполне хватает для того, чтобы сделать 12 задач (как 100 минут как раз хватает для выполнения всех 10 заданий Мальковского). Писали мы без перерыва и не сдавали отдельно задачу на пролог (сдали всё в самом конце).