Доказательство клауз. Лекция 7

Понятие высказывания
Определение
Высказывание – утверждение об изучаемых в рамках области знаний объектах, имеющее однозначно и точно определенное значение.
В классической (булевой, двузначной) логике высказываний значение может быть либо истинным либо ложным.
В русском языке под высказыванием понимается повествовательное предложение, относительно которого можно сказать, истинно оно или ложно.

Понятие формулы алгебры логики
(алгебры высказываний)
Определение
1) Логические переменные, символы 0 и 1 – формулы алгебры логики.
2) Если А – логическая формула, то (A) – логическая формула алгебры логики.
3) Если А, В – логические выражения, то , А⋅В, А∨В, А→В, А~В – формулы алгебры логики.

Основные определения
Опр. Пусть A(x1, ..., xn) - пропозициональная формула, где x1, ..., xn - входящие в нее пропозициональные переменные.
Конкретный набор истинности значений, приписанных переменным x1, ..., xn , называется интерпретацией формулы А.
Формула может быть истинной (иметь значение 1) при одной интерпретации и ложной (иметь значение 0) при другой интерпретации.
Опр. Формула, истинная при некоторой интерпретации, называется выполнимой. Формула, истинная при всех возможных интерпретациях, называется общезначимой (или тавтологией).
Опр. Формула, ложная при всех возможных интерпретациях, называется невыполнимой (или противоречием).
Опр. Две формулы назовем равносильными, если для любых наборов они принимают одинаковые значения.

Основные определения
Опр. Говорят, что формула В логически следует из формул A1, A2 ,..., An :
A1, A2 ,..., An ╞ B,
если формула В имеет значение 1 при всех интерпретациях, при которых формулы
A1, A2 ,..., An имеют одновременно значение 1.
Свойства:
1) A1, A2 ,..., An ╞ B, ⇒ A1, A2 ,..., An , ¬B ╞;
2) A1, A2 ,..., An ╞ ¬B, ⇒ A1, A2 ,..., An , B ╞;
3) A1, A2 ,..., An ╞ B→С, ⇒ A1, A2 ,..., An , B ╞ С – теорема о дедукции;
4) A╞ B, B╞ C, ⇒ A╞ С – правило силлогизма.

Доказательство от противного
1)
- Предположить, что существует такая интерпретация формул A1, A2 ,..., An, B, при которой
A1 =1, A2 =1,..., An=1; B = 0;
- прийти к противоречию.
2)
- Предположить, что существует такая интерпретация формул A1, A2 ,..., An, B, при которой
A1 =1, A2 =1,..., An=1, B = 1,
следовательно,
A1A2...An B = 1;
- прийти к противоречию.

Доказательство от противного

Доказательство от противного

Доказательство от противного

- Привести Ai, ¬B представлены в КНФ;
- составить конъюнкцию A1 A2...An¬B;
- последовательно применять правило резолюции
к дизъюнктам конъюнкции A1 A2...An¬B.
При последовательном применении правила резолюций происходит уменьшение числа переменных, вплоть до их полного исчезновения (если клауза верна).
Метод резолюций

Метод резолюций

Аксиоматический метод
Логика высказывания является расширением логики Буля. Поэтому все истинные тождества логики Буля автоматически становятся справедливыми клаузами логики высказываний.
Например, закон склеивания:
(A ∨ ¬В) (A ∨ В) = A
можно представить следующими справедливыми клаузами:
(A ∨ ¬В) (A ∨ В) |= A,
A |= (A ∨ ¬В) (A ∨ В).