что такое алгоритм эквивалентности двух правильно построенных формул

Question

каков алгоритм проверки того, что две WFF (правильно сформированные формулы) эквивалентны или нет, если «F» показывает «всегда ложно», а «T» показывает «всегда верно», также мы имеем {¬, ∧, ∨ , →, ↔}