Краткий ответ: формула тавтология.
Обоснование (коротко):
- Формула: $((P\to Q)\wedge (Q\to R))\to (P\to R)$.
- Натуральное доказательство: предположим $(P\to Q)\wedge (Q\to R)$ и дополнительно $P$. Из конъюнкции извлекаем $P\to Q$ и $Q\to R$. По modus ponens из $P$ и $P\to Q$ получаем $Q$; затем из $Q$ и $Q\to R$ — $R$. Значит при предположении $P$ следует $R$, т.е. $P\to R$. Поэтому вся формула истинна при любых значениях $P,Q,R$ — это тавтология.
- Альтернативно: проверить невалидность, т.е. рассмотреть отрицание
$$\neg (((P\to Q)\wedge (Q\to R))\to (P\to R))$$ которое эквивалентно
$$(P\to Q)\wedge (Q\to R)\wedge \neg (P\to R).$$ Преобразуя импликации: $(\neg P\vee Q)\wedge (\neg Q\vee R)\wedge (P\wedge \neg R)$. От $P$ и $\neg P\vee Q$ следует $Q$; от $Q$ и $\neg Q\vee R$ следует $R$; вместе с $\neg R$ получаем противоречие. Значит отрицание не может быть выполнено — исходная формула тавтологична.
Алгоритм автоматического доказательства/опровержения (рекомендации)
1. Прямой метод (для данной формулы простой и быстрый):
- Показать невыполнимость отрицания, как выше: привести к конъюнкции литералов/клауза и получить противоречие через дедукцию (одно- и двунаправленная подстановка).
2. Универсальный автоматический метод (подходит для произвольных пропозициональных формул):
- Проверить тавтологию как проверку невыполнимости отрицания, т.е. подать $\neg \varphi$ SAT-солверу.
- Преобразовать формулу в КНФ и использовать DPLL/CDCL SAT-решатель. Если $\neg \varphi$ невыполнима, то $\varphi$ — тавтология.
3. Метод резолюции:
- Взять клаузную форму $\neg \varphi$ и применить резолюцию; вывод пустой клаузулы означает тавтологию.
Разрешимость и сложность:
- Проблема проверка тавтологии в пропозициональной логике разрешима. Общая сложность: проверка тавтологии эквивалентна проверке невыполнимости SAT-отрицания и является coNP-полной; SAT — NP-полная.
- Точные ресурсы зависят от числа переменных $n$: тривиальный перебор по таблице истинности требует \(\(2^n\)\) проверок (экспоненциально).
Оптимизации на практике:
- Использовать CDCL-солверы с обучением клауз, unit propagation, эффектом pure-literal, эвристиками переменных (VSIDS).
- Для формул в импликационном или Horn-фрагменте — применять линейные по времени алгоритмы (проверка выводимости в Horn — за $O(n+m)$).
- Кэширование подформул, символьное упрощение и сат-предварительная обработка (удаление тавтологий, упрощение констант) уменьшают размер задач.
Заключение: формула $((P\to Q)\wedge (Q\to R))\to (P\to R)$ — тавтология; для автоматической проверки используйте доказательство невыполнимости $\neg \varphi$ через SAT (CDCL) или резолюцию; общая сложность задачи тавтологичности — coNP-полная.