Дискретная математика

Раздел 1. Математическая логика

Тема 1. Логика высказываний

Тема 2. Булевы функции

Тема 3. Логика предикатов

Тема 4. Метод резолюций

Тема посвящена рассмотрению метода доказательства того, что формула G является логическим следствием формул F1,F2,...,Fk, который называется методом резолюций. Отметим, что задача о логическом следствии сводится к задаче о выполнимости. Действительно, формула G есть логическое следствие формул F1,F2,...,Fk тогда и только тогда, когда множество формул {F1,F2,...,Fk,ØG} невыполнимо. Метод резолюций, если говорить более точно, устанавливает невыполнимость. Это первая особенность метода. Вторая особенность метода состоит в том, что он оперирует не с произвольными формулами, а с дизъюнктами (или элементарными дизъюнкциями).

§1. Метод резолюций в логике высказываний

§2. Подстановка и унификация

§3. Метод резолюций для логики первого порядка

§4. Эрбрановский универсум множества дизъюнктов

§5. Семантические деревья, теорема Эрбрана

§6. Полнота метода резолюций в логике предикатов

§7. Стратегии метода резолюций

§8. Применение метода резолюций.

§9. Метод резолюций и логическое программирование

Задачи

Ответы, указания и решения

1. Приведем решение задачи 1д. Рассмотрим множество T={F1,F2,ØG}. Каждую из формул этого множества приведем к КНФ, получим соответственно ØXÚØY, ØXÚYÚZ, X&ØZ. Тогда S равно {ØXÚØY,ØXÚYÚZ,X,ØZ}, а вывод пустого дизъюнкта есть ØXÚØY, X, ØØY, ØXÚYÚZ, ØXÚZ, Z, ØZ, □.


2. Приведем решение задачи 2.1. Рассмотрим высказывания: Х=«конгресс отказывается принять законы», Y=«забастовка не будет закончена», Z=«забастовка длится более месяца», U=«президент фирмы уйдет в отставку». Тогда предложения рассуждения 2.1 можно представить формулами F1=X®YÚ(Z&U), F2=X&ØY, G=Z. Сформируем множество T={F1,F2,ØG}, каждую из формул приведем к КНФ и получим множество дизъюнктов S={ØXÚYÚZ, ØXÚYÚU,X,ØY,ØZ}. Легко выдеть, что из S выводим □. Следовательно, рассуждение логично.


В задачах 2.4 и 2.5 рассуждение логично, а в задачах 2.2 и 2.3 – нелогично.


4. Указание. Воспользоваться алгоритмом унификации.


5. Дизъюнкт 5а имеет склейку, остальные не имеют.


6. Дизъюнкт в задаче 6б не имеет резольвент, в задаче 6а дизъюнкты имеют одну резольвенту Q(a,b), в задаче 6в – четыре ØP(a)ÚØQ(y,f(b))ÚQ(c,f(v)), ØP(x)ÚØQ(e,f(b))ÚQ(c,f(v)), ØP(x)ÚØP(a)ÚP(u), ØQ(y,f(b))ÚQ(c,f(v)).


7. В задаче 7б H0={a}, H1={a,b,g(a),g(b)}, H2={a,b,g(a),g(b),g(g(a)),g(g(b))}.


8. На рис. 4.9 изображены семантические деревья для S1, на рис. 4.11 – для S3. На рис. 4.10 изображено семантическое дерево для S2. (Эти множества дизъюнктов имеют и другие семантические деревья).


Рис. 4.9

Рис. 4.10


Рис. 4.11


9. Невыполнимое множество основных примеров есть

S1/={P(f(a),a,g(f(a),b),ØP(g(a),a,g(f(a,b)},

S2/={P(a),ØD(b)ÚÚL(a,b),ØP(a)ÚØQ(b)ÚØL(a,b),D(b),Q(b)},

S3/={ØK(a,b)ÚØL(b)ÚM(f(a)),ØK(a,b)ÚØL(b)ÚN(a,f(a)),ØM(f(a)),K(a,b),L(b)}.

10. Приведем решение задачи 10в. Составим множество {F1,F2,F3,ØG}. Каждую из формул приведем к сколемовской нормальной форме. Получим соответственно формулы

H1=("x)[(ØP(x)ÚQ(f(x))&(ØP(x)ÚS(x,f(x))],

H2=("y)[(R(a)ÚØQ(y))&(R(a)ÚØS(a,y))],

H3=P(b),

H4=("x)(P(x)ÚØR(x)).


Множество S будет состоять из семи дизъюнктов: S={ØP(x)ÚQ(f(x)), ØP(x)ÚS(x,f(x)), R(a)ÚØQ(y), R(a)ÚØS(a,y)), P(b), P(x),ØR(x)}. Выводом пустого дизъюнкта будет последовательность


D1=ØP(x)ÚQ(f(x)), D2=P(x), D3=Q(f(x)), D4=ØR(x), D5=R(a)ÚØQ(y), D6=ØQ(y), D7=□.


Отметим, что D3 следует по правилу резолюций из D1,D2, D6 – из D4 и D5, а D7 – из D3 и D6. Дизъюнкты D1,D2,D4,D5 принадлежат S.


11. Приведем решение задачи 11.2. Пусть символы одноместных предикатов F,G и S интерпретируются следующим образом

F(x): «х – болельщик «Спартака»,

G(x): «х – студент нашей группы»,

S(x): «х – спортсмен».

Тогда рассуждение 11.2 можно представить формулами:

F=("x)(G(x)®F(x))&($y)(G(y)&S(y)),

G=($x)(F(x)&S(x)).

Составим множество формул {F,ØG} и каждую из них приведем к сколемовской нормальной форме. Получим формулы

H1=("x)(ØG(x)ÚF(x))&G(a)&S(a)

H2=("x)(ØF(x)ÚØS(x)).

Множество дизъюнктов S равно {ØG(x)ÚF(x),ØF(x)ÚØS(x),G(a),S(a)}. Пустой дизъюнкт из множества S выводится очевидным образом.


12. Рассуждения 12.1, 12.4 логичны, остальные рассуждения нелогичны.

Раздел 2. Теория графов

Тема 5. Раскраски

Тема 6. Ориентированные графы и сети


Fair.ru Ярмарка сайтов
Rambler's Top100 Submitter.ru - Free promoting

Дизайн: Alex © 2002
Все вопросы и предложения можно направлять по адресу cad@mail.ustu.ru