14
Formal Logic
At this point all occurrences of statement letters have truth values, as follows:
A–T B–T
B–F A–T
(A S B)
S
(B′ S A′)
T
F
This terminates the loop. In the final step of the algorithm, B now has an assignment of both T and F, so the algorithm decides that (A S B) S (B′ S A′)
is a tautology. Actually, we learned this earlier (in Practice 7(d)) by building a
truth table.
Algorithm TautologyTest decides whether wffs of a certain form, namely,
those where the main logical connective is S, are tautologies. However, the process of building a truth table and then examining all the truth values in the final
column constitutes an algorithm to decide whether an arbitrary wff is a tautology.
This second algorithm is therefore more powerful because it solves a more general
problem, but algorithm TautologyTest is usually faster for those wffs to which it
applies.
ReMIndeR
Algorithm TautologyTest
applies only when the
main connective is S.
Formal Logic
At this point all occurrences of statement letters have truth values, as follows:
A–T B–T
B–F A–T
(A S B)
S
(B′ S A′)
T
F
This terminates the loop. In the final step of the algorithm, B now has an assignment of both T and F, so the algorithm decides that (A S B) S (B′ S A′)
is a tautology. Actually, we learned this earlier (in Practice 7(d)) by building a
truth table.
Algorithm TautologyTest decides whether wffs of a certain form, namely,
those where the main logical connective is S, are tautologies. However, the process of building a truth table and then examining all the truth values in the final
column constitutes an algorithm to decide whether an arbitrary wff is a tautology.
This second algorithm is therefore more powerful because it solves a more general
problem, but algorithm TautologyTest is usually faster for those wffs to which it
applies.
ReMIndeR
Algorithm TautologyTest
applies only when the
main connective is S.