lThere is no tool that can determine whether an arbitrary predicate logic formula is
valid.
lIf there were, the halting problem would be
solvable.
lThis is because the computation by a Turing machine can
be captured as an appropriate
logical formula, one which is valid iff the Turing machine
fails to halt.