Термины Flashcards
Логика Высказываний (ЛВ, Пропозициональная логика)
Это более простой уровень логики, работающий с высказываниями (пропозициями) как с неделимыми атомами. Высказывание — утверждение, которое может быть истинным (И) или ложным (Л). Основное внимание уделяется зависимости истинности сложных высказываний от истинности простых и от логических связок (И, ИЛИ, НЕ, ЕСЛИ…ТО, ТОГДА И ТОЛЬКО ТОГДА).
Основные элементы ЛВ
Пропозициональные переменные (P, Q, A, B…), Логические связки (¬, ∧, ∨, →, ↔), Скобки.
Логика предикатов (ЛП)
Расширение Логики Высказываний, позволяющее анализировать внутреннюю структуру простых высказываний. Вводит понятия объектов (индивидов), их свойств и отношений между ними. Ключевое нововведение — кванторы (‘для всех’ ∀, ‘существует’ ∃).
Формальная система
Строго определённая среда для рассуждений с алфавитом, синтаксисом, часто аксиомами, и правилами вывода. Правила вывода позволяют из имеющихся формул получать новые (например, modus ponens: из A и A → B следует B).
Сигнатура (в логике)
Набор символов, определяющий ‘алфавит’ логического языка: символы констант, функций, предикатов (отношений) с указанием их арности (числа аргументов). Задает синтаксис, но не смысл.
Интерпретация (в ЛП)
Процесс и результат придания смысла символам сигнатуры в предметной области (универсуме). Включает:
1) Непустой универсум (множество объектов)
2) Сопоставление константам элементов универсума
3) Сопоставление функциональным символам функций над универсумом
4) Сопоставление предикатным символам отношений над универсумом.
Модель (в логике)
Интерпретация, в которой данная формула (или набор формул) является истинной. Если формула Ф истинна в интерпретации I, то I - модель для Ф (I удовлетворяет Ф).
Выполнимость (формулы)
Свойство формулы, означающее существование хотя бы одной модели для неё (т.е. интерпретации, где она истинна). Невыполнимая формула называется противоречивой.
Общезначимость (формулы)
Свойство формулы, означающее её истинность во всех возможных интерпретациях для данной сигнатуры. Выражает универсальный логический закон.
Тавтология
Формула (обычно ЛВ), истинная при любой интерпретации её логических связок или при любых значениях истинности входящих в неё переменных. Пример: A ∨ ¬A. В ЛВ совпадает с общезначимостью.
Логическое (семантическое) следование (Γ ⊨ φ)
Формула φ логически следует из множества формул Γ, если во всех интерпретациях (моделях), где истинны все формулы из Γ, формула φ также истинна. Обозначение: Γ ⊨ φ. Пример: {P(a)→Q(a), P(a)} ⊨ Q(a).
Тавтологическое следствие
Аналог логического следования для ЛВ. Формула B является тавтологическим следствием формулы A, если во всех строках таблицы истинности, где A истинно, B тоже истинно.
Совместность (набора формул)
Свойство набора формул, означающее существование хотя бы одной модели (интерпретации), в которой все формулы из этого набора одновременно истинны. Эквивалентно выполнимости конъюнкции всех формул набора.
Выводимость (Γ ⊢ φ)
Свойство формулы φ быть выводимой из множества формул Γ в рамках формальной системы, т.е. существование конечного доказательства φ из Γ с использованием аксиом и правил вывода системы. Обозначение: Γ ⊢ φ. Пример: ¬¬A ⊢ A.
Непротиворечивость (синтаксическая)
Свойство набора формул (или формальной системы), означающее невозможность вывести из него противоречие (например, формулу вида A ∧ ¬A).
Полнота (логической системы)
Свойство логической системы, означающее, что любая общезначимая (семантически истинная) формула является выводимой (доказуемой) в этой системе. Пример: Классическая ЛВ полна.
Разрешимость (логической системы)
Свойство системы, означающее существование алгоритма, который для любой формулы может определить, является ли она теоремой (выводима ли она в системе). Если такого алгоритма нет, система неразрешима. Пример: Арифметика Пеано неразрешима.
Предваренная нормальная форма (ПНФ)
Стандартная форма формулы ЛП, где все кванторы (∀, ∃) вынесены в начало, а за ними следует формула без кванторов (матрица). Любую формулу можно привести к эквивалентной ПНФ.
Сколемовская нормальная форма (СНФ)
Форма формулы в ПНФ, где устранены кванторы существования (∃) путем введения новых (сколемовских) функций или констант. Не эквивалентна исходной, но сохраняет выполнимость.
Унификация
Процесс нахождения подстановки (значений для переменных), которая делает два терма или выражения синтаксически идентичными. Пример: Унификация P(a, x) и P(a, b) дает подстановку x = b.
Правило (метод) резолюций
Основной метод автоматического доказательства в ЛП, особенно для формул в клаузальной форме. Основан на правиле: из (A ∨ B) и (¬A ∨ C) следует (B ∨ C). Часто используется для доказательства от противного.
Дизъюнкт / Клауза
Логическое выражение, представляющее собой дизъюнкцию (логическое ИЛИ, ∨) одного или нескольких литералов.
Литерал
Атомарная формула (например, P(x), Q) или её отрицание (¬P(x), ¬Q). Положительный литерал - без отрицания, отрицательный - с отрицанием.
Фраза Хорна (Horn Clause / Клауза Хорна)
Дизъюнкт (клауза), содержащий не более одного положительного литерала. Примеры: ¬P ∨ ¬Q ∨ R (правило R :- P, Q), R (факт), ¬P ∨ ¬Q (запрос ?- P, Q).
Пролог-программа
Программа на языке логического программирования Пролог. Состоит из фактов и правил (хорновских фраз). Выполнение - попытка логического вывода цели с помощью SLD-резолюции и унификации.
Запросы и решения в Прологе
Запрос: Цель (goal), которую пользователь задает Пролог-системе для доказательства. Решения: Ответы системы, подтверждающие истинность запроса (возможно, с подстановками переменных) или сообщающие о неудаче (‘false’/’no’).
