Математическая Логика, 03 лекция (от 26 сентября)
Материал из eSyr's wiki.
Предыдущая лекция | Следующая лекция
Слайды: http://mathcyb.cs.msu.su/paper/zakh/LectLog3.pdf http://mathcyb.cs.msu.su/paper/zakh/LectLog4.pdf
418, 419 группы — лекция 29 сентября 10:30Ю ауд. 613 420—428, 441 — лекция 2 октября 14:35, П-5
Лекция 3. Выполнимые и общесзнач. формулы. Моедли. Логическое следование. Проблема общезначимости. Семантические таблицы.
Проблема общезн. непростая проблема, требующая разработки спец. аппарата, лектор расскаже о предпосылках созд. этого аппарата, самый простой вариант, расск. про вывод в табицах.
После введения понятия фолмуры можно классиф формуцлы:
- Ф-ла может быть итсинной всегдПА, иногда, никогда
Формула выпонлима, елси он выполн на данном наборе переменных. То есть, ф-ла выполнима, если она не совсем ложна, выполняется при нек-ром наборк параметров. Бывает, что ф-ла выполняется для оюбого набора переменных, тогда она истинна. Формула просто выполнима, которая выполнима в какой-либо интерпретации. Если же формула истинна на любой интерпретации, то она является тожд. истинна, или общезначима, то есть верна везде и свюду при любыъ значениях переменных. Если же формула никогда не выполняется, то она противоречива, неверна.
Для проверки выполнимости достаточно придумать один пример, но общезначимость надо проверять на всех интерп., как это сделать?
Выполнимые формулы — важные вещи, так как именно они несут знания. Выполнимые формы — формы предст. знаний. Но общезначимые формулы — банальны, не несут никакой информации. Но вместе с тем, они для нас самые интересные. Почему? Какая роль им отводится?
Пусть у нас есть множество замк. формул. Тогда интерп., в которой выполнчются все эти формулы, называется моделью для этого множества. Мы оговорим множество утв., они образуют БЗ. И тогда возникает вопрос, есть ли мир, в которой выполняется эта БЗ? Такой мир есть модель для БЗ. Таких миров может быть много.
Почему для пустогно множества формул интерп любая? Потому что определение сокращённое, на самом деле там импликация "для любой формулы если она в Г то она должна выполняться в модели Г". Тогда импликация верна и в том случае, если левая часть ложна.
Сами по себе модели не так интересны. Гораздо более важно понятие логического следования. Пусть есть база Г, есть замкнутая формула. Эта флормула называется лог. следствием, если каждая модели Г есть модель для формулы. Логические следствия — производные знания. Есть причинно-следст. связь, но важен факт следствия, а не механизм получения связи. Это одна из важн. задач — получение следствий.
Обозначения
- Г |= φ — φ — логическое следствие Г
- следствиями пустой БЗ являются общезначимые формулы, поэтому для обозн. общезн. будем исп. |= φ
Насколько это применимо на практике?
Пример:
- Даша любит Сашу
- Саша любит пиво
- Паша любит пиво и всех тех, кто любит то, что любит Паша
Вопрос: любима ли Даша?
Психологи изучали, с какого этапа человек способен к широкой аналитической деятельности? Ребёнок не может установить причинно-следственные связи до 10—11 лет. Можем ли мы сказать, что ребёнок 8 лет не обладает интеллектом? Нет. Следовательно, можно создать систему, которая может системно реать подобные задачи.
Решение. Сформируем алфавит:
- Даша
- Саша
- Паша
- пиво
Предикаты
- L(x, y) "x любит y"
Условия задачи на языке предикатов:
- L(Даша, Саша)
- L(Саша, пиво)
- L(Паша, пиво) & (∀x L(Паша, х) & (∀y L()))
Любима ли Даша: ∃x L(x, Даша)
Рассмотрим аппарат для решения задачи.
Теорема о логическом следствии.
Общезн. формулы — это каналы причинно-следст. связи, по которым передаются знания. Важно определять эти каналы и уметь извлекать из них знания. Следовательно, будем заниматьсч робелмой общезначимости: выяснять, являетсмя ли данная формула общезначимой?
Проверка выполн./общезн. для любой формулы сводится к проверке выполн./общезн. замкнутой формулы.
Прверка перебором невозможна, так как существует формула, которая истинна для любой конечной интерп. и не общезначима.
Следовательно, перебором проверить нельзя, и нужны более извращённые способы.
Можно доказывать методом от противоположного за конечного количества шагов, правда, пока непонтно, как эти шаги систематизировать.
Пример. Проверить общезначимость формулы φ = ∃xP(x) → ∀xP(x)
Доказательство:
≠ φ | |
= ∃xP(x) | ≠ ∀xP(x) |
= P(x)[d] | ≠ P(x)[d2] |
I: d1, d2, P(d1) = true, P(d2) = false
То есть, разбирая формулу, можно построить контрпример, или показать, что его нет.
Систематизируем этот способ проверки формул. Попробуем ввести способ проверки, который независит от нашей квалификации — семант. таблицы.
Есть и другие способы (напр., секвенциальный вывод), их мы рассмотрим в 4/4 курса.
Лекция 4.
Представим, что у нас в формуле нет кванторов, то есть это ыактически нечто вроде булевой формулы. Как её проверить? Достаточно перебрать все возм. значния, и для этого хватит аппарата булевой алгебры. С кванторами это не прокатит. Важная сост. лог. вывода — умение пользоваться подстановками. ДАлее мы рассмотрим, каковы правила табл. вывода, преобр. одни таблицы в другие, и по каким законам ведётся игра под называнием табл. вывод. И обоснуем, что если не выигрываем мы, то можем обосновать общезначимость формлы.
Подстановка — всякое отобр. из множества перем. в множество термов.
Область подстановки — те перем., которые изм. в результате подстановки.
Если изм. конеч. число перем., то подстановка конечна.
Формы прочтения правил табличного вывода:
- Верхняя таблица выполнима ↔ выполнима хотя бы одна нижняя
- Верхняя таблица невыполнима ↔ ни одна нижняя невыполнима
Мнемон. обозн правил:
- первая буква — из левой или правой части таблицы правило
- вторая — какая основная операция
Вопрос выполнимости таблиц сводится к вопросы выполнимости более простых таблиц.
Символ, который имеет незапятнанную репутацию, я его впервые здесь ввожу.
У меня есть константа. Дам-ка я ей свеженькое имя с.
Этот метод можно до бесконечности тянуть, поэтому нужны методы для выяснения бесконечности вывода, предохранители.
|
|
Ссылки
Официальная страница курса | Задачи
Проведение экзамена | Решение задач: Решение задач методички | Решение задач варианта экзамена 2004 года | Алгоритмы решения задач