Стратегии доказательства пропозициональных тавтологий?

Question

Ввод представляет собой строку символов с (любым) проверенным синтаксисом, а выход - ИСТИНА или ЛОЖЬ.

Моя идея была пост-фиксированное представление логических выражений, написанных с помощью AND, XOR и TRUE, но я, наконец, понял, что шаблоны будет сложнее распознать в post-fix.

Примеры:

р, то^ можно записать ИСТИНА XOR р (исключающее ИЛИ (р, д)) сокращенно 1 + р + PQ

р равносильна д можно записать сокращенно 1 + р + д

НЕ р сокращенно 1 + р

р ИЛИ д сокращенно р + д + рд

правила в этом булева кольца такое же, как и в обычной алгебре, с двумя правилами

• р + р = 0
• pp = p

, и эти правила вместе с коммутациями отвечают за все сокращения, что приведет к «1», если строка соответствует тавтологии. Тавтологию Модусные поненс,

((р, то ^) и р) ПОДРАЗУМЕВАЕТ д,

должен сначала быть замещен, как указано выше, а затем расширенный путем умножения дистрибутивно, и последний раз быть упрощена. Прямое замещение ПОДРАЗУМЕВАЕТ дает:

1+((1+f+fg)f)+((1+f+fg)f)g = 
= 1+ f+ff+fgf +(f+ff+fgf)g = 
= 1+ f+f+fg + fg+fg+fg = 
= 1+ fg +fg+fg+fg = 1 

Когда тавтологическое выражение записано как элемент в булева кольцах это уменьшает механически 1. Другое выражение сводится к алгебраически простому выражению.

Это хорошая стратегия? Какие стратегии используются в информатике?

Answer 1

Как обсуждался в этом overview paper, произвольная пропозициональная формула может быть преобразована в кнфе (CNF) таким образом, что она имеет только полиномиальный больший размер и невыполнимо тогда и только тогда, оригинальная формула была тавтологией.

Практические инструменты для преобразования формулы в CNF включают bool2cnf и bc2cnf.

SAT solvers для проверки недостоверности CNF включает CryptoMiniSat и Lingeling.

См. related post, где показано, как обрабатывать формулы пропозиции с использованием решателя SAT.