A less serious problem is that it’s possible to specify redundant rules. The most extreme form is a rule which is always satisfied, like “Probability or not Probability”. These are called tautologies. The problem of identifying tautologies is in some sense dual to that of identifying unsatisfiability. Instead of looking for rules which can never be satisfied we’re looking for ones which can always be satisfied.
A tautology is a special case of a consequence. One statement is a consequence of others if it is always satisfied whenever they are. A tautology is a statement which is a consequence of the empty set of statements. The question of whether a statement in our language is a tautology is decidable, at least in a theoretical sense. More generally, the question of whether one statement is a consequence of a list of other statements is decidable, in the same sense.