X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
Формула φ сигнатуры Σ называется бескванторной, если она не содержит кванторов. Бескванторная формула φ является дизъюнктивной (конъюнктивной) нормальной формой, если она получается из некоторой формулы ψ АВ, находящейся в ДНФ (КНФ), заменой всех пропозициональных переменных x1,…,xn на некоторые атомарные формулы φ1,…,φn сигнатуры Σ соответственно.
Говорят, что формула φ сигнатуры Σ находится в пренексной нормальной форме (ПНФ), если она имеет вид Q1x1…Qnxnψ, где Qi, ‑ кванторы (1≤i≤n), n ψ – дизъюнктивная нормальная форма.
Теорема 1. Для любой формулы φ сигнатуры Σ существует ПНФ ψ, эквивалентная формуле φ.
Опишим алгоритм приведения формулы к ПНФ:
выражаем импликацию, участвующую в построении формулы, через дизъюнкцию и отрицание, используя эквивалентность φ→ψ≡¬φ∨ψ;
используя законы де Моргана ¬(φ∧ψ)≡¬φ∨¬ψ, ¬(φ∨ψ)≡¬φ∧¬ψ
и эквивалентности ¬xφ≡x¬φ, ¬xφ≡x¬φ,
переносим все отрицания к атомарным подформулам и сокращаем двойные отрицания по правилу ¬¬φ≡φ;
приводим формулу к виду Q1x1…Qnxnψ , где Qi, ‑ кванторы (1≤i≤n), n ψ – бескванторная формула, пользуясь эквивалентностями
- Введение
- Программа курса математическая логика и терия алгоритмов
- Логическое следствие в алгебре высказываний
- 2.1.3. Эквивалентные формулы алгебры высказываний
- 2.1.4. Дизъюнктивные и конъюнктивные нормальные формы в алгебре высказываний
- 2.1.5. Совершенные дизъюнктивные и конъюнктивные нормальные формы
- Исчисление высказываний
- Определение формального исчисления
- Система аксиом и правил вывода
- Теорема о дедукции в исчислении высказываний
- Теорема о замене в исчисления высказываний
- Свойства выводимых и эквивалентных формул исчисления высказываний
- Основные эквивалентности исчисления высказываний
- Полнота и непротиворечивость исчисления высказываний
- Логика предикатов
- Алгебраические системы
- Пример 3. Построить подсистему алгебраической системы , порожденную множествомХ:
- Формулы логики предикатов
- Истинность формулы логики предикатов в алгебраической системе
- 2.3.4. Логическое следствие в логике предикатов
- 2.3.5. Эквивалентные формулы логики предикатов
- 2.3.6. Пренексная нормальная форма в логике предикатов
- X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
- X(φ∧ψ)≡xφ∧ψ, X(φ∨ψ)≡xφ∨ψ,
- Xφ≡X(φ)xφ≡X(φ)
- 2.4. Исчисление предикатов
- 2.4.1. Система аксиом и правил вывода
- 2.4.2. Эквивалентные формулы исчисления предикатов
- 2.4.3. Теорема Геделя о полноте. Непротиворечивость исчисления предикатов
- Элементы теории алгоритмов
- 2.5.1. Машины Тьюринга
- 2.5.2. Примитивно рекурсивные функции
- 2.5.3. Частично рекурсивные функции
- Задания для домашних и контрольных работ
- 3.1. Совершенные дизъюнктивные нормальные формы, совершенные конъюнктивные нормальные формы
- 3.2. Логическое следствие в алгебре высказываний
- Логическое следствие в логике предикатов
- Частично рекурсивные функции
- Список литературы
- Основная литература
- 4.2. Дополнительная литература
- Содержание