# Mechanization of Mathematics

Its been a while since I took my theory course, but I recall that Hilberts Decision problem was shown to be false.

By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the Entscheidungsproblem can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic.

From Wikipedia.

But In my AI course, we learned of an algorithm to prove or disprove new statements using the axioms known as Resolution by refutation. Simply take the a negation of the statement you want to prove, and use the axioms to show it either leads to an empty clause (true) or non-empty clause (false).

So my question is: What am I missing from these two seemingly contradictory statements? On one hand the literature states there exists no algorithm to determine if a statement is provable from the axioms, and on the other hand, I am presented with an algorithm that proves (or disproves) a statement from the axioms. What am I confused or incorrect about here?