Методические указания к выполнению лабораторных работ 1-3 по дисциплине «Математическая логика и теория алгоритмов»

Теорема. Резольвента является логическим следствием порождающих ее дизъюнктов, то есть, ╞. Метод резолюций доказательства невыполнимости формулы состоит в том, что эта формула представляется в КНФ и к ней конъюнктивно присоединяются все возможные резольвенты ее дизъюнктов и получаемых в процессе доказательства резольвент. Полнота метода резолюций состоит в том, что он гарантирует получение для формулы следствия false, если невыполнима. Если же, перебрав все возможные резольвенты формулы , мы не нашли пустую резольвенту, то не является невыполнимой. Вывод пустого дизъюнкта может быть наглядно представлен с помощью дерева вывода, вершинами которого являются или исходные дизъюнкты, или резольвенты, а корнем – пустой дизъюнкт. Пусть задано множество дизъюнктов . Для заданного множества дизъюнктов дерево поиска представлено на рис. 3. Пример 1. Доказать правильность логического вывода. Если я пойду завтра на первое занятие, то должен буду встать рано, а если я пойду вечером на танцы, то лягу спать поздно. Если я лягу спать поздно, а встану рано, то вынужден довольствоваться пятью часами сна. Я просто не в состоянии 30 обойтись пятью часами сна. Вывод: я должен или пропустить завтра первое занятие, или не ходить на танцы. Введем следующие обозначения: - “Я пойду на первое занятие”; - “Я должен встать рано”; - “Я пойду на танцы”; - “Я лягу спать поздно”; - “Я могу обойтись пятью часами сна”. Рис. 3. Дерево поиска Данной задаче соответствует следующее формальное описание: ; ; ╞ . Так как доказательство проводится методом от противного, то вывод берется с отрицанием. Исходные посылки и вывод, взятый с отрицанием, представим в виде множества дизъюнктов и будем формировать возможные резольвенты с целью получения нулевой резольвенты. 31 1. ; 2. ; 3. ; 4. ; 5. C; 6. D ; 7. (1,5); 8. (2,6); 9. (3,4); 10. (7,9). 11. Нулевая резольвента () (8,10). Получение нулевой резольвенты свидетельствует о невыполнимости исходной формулы, то есть, мы пытались всеми возможными методами подтвердить ложность вывода, но нам это не удалось. Следовательно, вывод является правильным. Как следует из этого примера, формирование резольвент не является однозначной процедурой. Существует много различных подходов к реализации метода резолюций, которые позволяют формализовать этот процесс. 2.3.1. Метод насыщения уровня Метод насыщения уровня состоит в вычислении всех резольвент всех пар дизъюнктов из множества дизъюнктов , добавлении этих резольвент к множеству , вычислении всех следующих резольвент и повторении этого процесса, до тех пор, пока не найдется пустой дизъюнкт . Проиллюстрируем рассмотренный метод на примере множества дизъюнктов 1. 2. 32 3. 4. _________________________ : 5. (1,2) 6. (1,3) 7. (1,4) 8. (1,4) 9. (2,3) 10. (2,3) 11. (2,4) 12. (3,4) ___________________________ : 13. (1,7) 14. (1,8) 15. (1,9) 16. (1,10) 17. (1,11) 18. (1,12) 19. (2,6) 20. (2,7) 21. (2,8) 22. (2,9) 23. (2,10) 24. (2,12) 25. (3,5) 26. (3,7) 27. (3,8) 33 28. (3,9) 29. (3,10) 30. (3,11) 31. (4,5) 32. (4,6) 33. (4,7) 34. (4,8) 35. (4,9) 36. (4,10) 37. (5,7) 38. (5,9) 39. Нулевая резольвента () (5,12) Этот пример наглядно демонстрирует, что при использования метода насыщения уровня генерируется много повторяющихся дизъюнктов, а также дизъюнктов, являющихся тавтологиями. Так как тавтология всегда истинна, то вычеркивая ее из невыполнимого множества дизъюнктов, мы сохраняем невыполнимость множества дизъюнктов. Для сокращения избыточности могут использоваться различные стратегии, например, стратегия вычеркивания. 2.3.2. Стратегия вычеркивания Дизъюнкт называется поддизъюнктом (или поглощает ), если является некоторой частью дизъюнкта . При этом называется наддизъюнктом для . Например, если , , то - поддизъюнкт, а наддизъюнкт для . Стратегия вычеркивания зависит от того, как удаляются 34 из множества, полученного методом насыщения уровня, тавтологии и наддизъюнкты. Стратегия вычеркивания будет полной, если ее использовать вместе с методом насыщения уровня таким способом: сперва выписываются все дизъюнкты по порядку; затем вычисляются резольвенты путем сравнения каждого дизъюнкта с дизъюнктом , который стоит после . Если эта резольвента не тавтология и не поглощается каким-нибудь дизъюнктом из списка, то она записывается в конец списка. В противном случае она вычеркивается. Очевидно, при этом не выписывается повторно один и тот же дизъюнкт. Применение метода резолюций к примеру, рассмотренному в методе насыщения, дает следующий результат: 1. 2. 3. 4. ____________________________ : 5. (1,2) 6. (1,3) 7. (2,4) 8. (3,4) ____________________________ Нулевая резольвента () (5,8) Однако этот метод, уменьшая затраты памяти для реализации, увеличивает количество вычислений, поскольку помимо генерации всех дизъюнктов необходимо проверять, 35 являются ли полученные дизъюнкты тавтологиями или поддизъюнктами других дизъюнктов. Для уменьшения количества вычислений могут быть использованы следующие методы: метод семантической резолюции, лок-резолюции, линейной резолюции. 2.3.3. Метод лок- резолюции Суть метода лок-резолюции состоит в использовании индексов для упорядочения литер в дизъюнктах из данного множества дизъюнктов. Для каждого вхождения литеры в вводится некоторое целое число. Разные вхождения одной и той же литеры могут быть индексированы по-разному. Разрешается удалять только литеры с наименьшим индексом в каждом из дизъюнктов. Литеры в резольвентах наследуют свои индексы из посылок. Если литера в резольвенте может унаследовать более одного индекса, то ей ставится в соответствие наименьший индекс. Рассмотрим следующие два дизъюнкта (1) (2) Так как индекс 1 в ниже, чем индекс 2 в , то удаляется . Аналогично, так как индекс 3 в ниже, чем индекс 4 в, то можно удалить . Применяя правило резолюции к дизъюнктам (1) и (2) по и получаем (3) Литера и одна и та же. Так как индекс 2 меньше индекса 4, то оставляем (4) Дизъюнкт (4) называется лок-резольвентой дизъюнктов (1) и (2). 36 Под лок-резолюцией понимается последовательное получение лок-резольвент из данного множества дизъюнктов и вновь получаемых дизъюнктов. Рассмотрим применение метода лок-резолюции для еще одного примера, рассмотренного в методе насыщения и методе вычеркивания: 1. 2. 3. 4. Проиндексируем вхождение каждой литеры в : 1. 2. 3. 4. Из дизъюнктов(1)-(4) можно получить только одну лок-резольвенту 5. (3,4) Из дизъюнктов (1)-(5) получаются только две лок-резольвенты 6. (1,5) 7. (2,5) 8. Нулевая резольвента () (6,7) Применяя правило резолюции к дизъюнктам (6) и (7), получаем пустую резольвенту. Таким образом, для получения нулевой резольвенты были сгенерированны только три лок-резольвенты. Результативность лок-резолюции не зависит от способа индексации литер. Изменим порядок индексации 37 1. 2. 3. 4. Из (1) и (3) получаем: 5. (1,3) 6. (1,4) 7. (2,3) 8. (2,4) 9. . Нулевая резольвента () (5,8) КОНТРОЛЬНЫЕ ВОПРОСЫ И ЗАДАНИЯ

Похожие:

	Учебно-методический комплекс по дисциплине математическая логика и теория алгоритмов Курс математическая логика и теория алгоритмов обеспечивает приобретение знаний в соответствии с государственным образовательным...		Вопросы к экзамену по курсу «Математическая логика и теория алгоритмов» Методические указания предназначены для студентов, обучающихся по направлению 020400. 68 «Биология», магистерская программа 020400....
	Программа дисциплины «Информатика, математическая логика и теория... Программа предназначена для преподавателей, ведущих данную дисциплину, учебных ассистентов и студентов направлений подготовки 231000....		«Разработка алгоритмов и программирование на языке Pascal» Лабораторный практикум содержит методические указания к выполнению лабораторных работ по алгоритмизации и программированию на языке...
	Методические указания по выполнению контрольных работ для экономических специальностей Методические указания по выполнению контрольных работ по дисциплине "Экономическая теория" для студентов экономических специальностей–...		Методические указания к выполнению контрольных работ по дисциплине “ Методические указания к выполнению контрольных работ по дисциплине “Основы внешнеэкономической деятельности” для студентов экономических...
	Программа вступительных испытаний по дисциплине «Математика» Курс математическая логика и теория алгоритмов обеспечивает приобретение знаний в соответствии с государственным образовательным...		Методические указания по выполнению контрольных работ по дисциплине Методические указания по выполнению контрольных работ по дисциплине «Правовые основы российского государства» для студентов по специальности...
	Методические указания к выполнению контрольных работ по дисциплине «Информатика» Задания и методические указания к выполнению контрольных работ по дисциплине «Информатика». Екатеринбург, фгаоу впо «Российский государственный...		Рабочая программа по дисциплине В. В математическая логика и теория алгоритмов Рабочая программа составлена на основе фгос впо и учебного плана мгту по направлению 090900. 62 Информационная безопасность
	Рабочая программа по дисциплине В. В математическая логика и теория алгоритмов Рабочая программа составлена на основе фгос впо и учебного плана мгту по направлению 090900. 62 Информационная безопасность		Факультет экспертизы и товароведения методические указания к выполнению... «Нам дан во владение самый богатый, меткий, могучий и поистине волшебный русский язык». (К. Г. Паустовский)
	Сборник методических указаний для студентов по выполнению лабораторных работ дисциплина «химия» Методические указания для выполнения лабораторных работ являются частью основной профессиональной образовательной программы Государственного...		Рефератов по курсу «Математическая логика и теория алгоритмов» Темпоральные логики высказываний линейного времени и вычислительных деревьев: их синтаксис и семантика
	Методические указания по выполнению курсов ых работ по дисциплине «теория управления» Методические указания предназначены для выполнения курсовой работы студентами направления подготовки бакалавриат 081100. 62 «г осударственное...		Методические указания по выполнению реферативных работ по дисциплине «История и философия науки» Методические указания к выполнению реферативных работ аспирантов и соискателей по дисциплине «История и философия науки» /Уфимск...