- Determine the number of variables in the expression and store this in something like "num_vars".
- Find all bit_strings (sequences of '0s' and '1s') which have the same length as num_vars. Store each of these in an ordered structure.
- Number, or order the variables in the logical expression. For instance, A is always the first variable, B always the second, and so on.
- Set the current bit string as the 0th element of the bit_string ordered structure.
- For all variables in the expression, replace the nth_variable of a clone of the expression with the nth_element of the current bit string. E. G. if the current bit string is 0011, then replace the variable 'A' with '0', 'B' with '0', 'C' with '1', and 'D' with '0'.
- Calculate whether the resulting formula (with just connectives and '0s' and '1s') is a tautology or not. If it is not a tautology, then halt. The expression is not a tautology. Otherwise continue.
- If the current bit string is not the last bit_string in the bit_string list, then set the current bit_string to the successor of the bit_string (bit_string + 1), and then goto 5. Otherwise, halt, the formula is a tautology.
Example: CaCbc
Three variables (step 1).
['000', '001', '010', '011', '100', '101', '110', '111'] (step 2)
a - 0, b - 1, c - 2 (step 3)
current_bit_string = 0 (step 4)
C0C00 (step 5)
1 (step 6) and thus we continue
current_bit_string = 1 (step 7)
C0C01 (step 5)
1 (step 6)
current_bit_string = 2 (step 7)
C0C10 (step 5)
1 (step 6)
current_bit_string = 3 (step 7)
C0C11 (step 5)
1 (step 6)
current_bit_string = 4 (step 7)
C1C00 (step 5)
1 (step 6)
current_bit_string = 5 (step 7)
C1C01 (step 5)
1 (step 6)
current_bit_string = 6 (step 7)
C1C10 (step 5)
0 Halt this is not a tautology. (step 6)
Note step 2. The bit_strings can appear in any order so long as we have all of them. If we have some more knowledge about when a formula is not a tautology, we might thus make the algorithm more efficient using that knowledge, by generating all bit strings and re-ordering them according to when when an expression is not a tautology. Or just by using that knowledge in another way.
For instance, if the expression only has conditionals, and we're working in prefix notation, then if an expression is not a tautology, then the formula is not a tautology when at some instance where the last variable instantiates as 0. Thus, we might re-order the ordered structure of bit_strings as follows such that those bit_strings where '0' is the last element come first.
['000', '010', '100', '110', ...]
Thus, we end up as more likely to find those cases where a formula is not a tautology more quickly. And actually, in this case where we only have conditional symbols, we do NOT need to check any of the cases where the last element of the bit_string equals '1'. We only need to check the cases where the last element of the bit_string equals '0'.