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

<blockquote>
  <p>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 <strong>algorithm to decide whether a given statement is provable from the axioms using the rules of logic.</strong></p>
</blockquote>

<p>From <a href="https://en.wikipedia.org/wiki/Entscheidungsproblem" rel="noreferrer">Wikipedia</a>.</p>

<p>But In my AI course, we learned of an algorithm to prove or disprove new statements using the axioms known as <a href="http://athena.ecs.csus.edu/~logicp/unification-resolution/resolution-refutation.html" rel="noreferrer">Resolution by refutation</a>. 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).</p>

<p>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?</p>

<automated-theorem-proving><resolution>
Mechanization of Mathematics
abrahimladha
# Mechanization of Mathematics

(Asked by: username_0 on 2016-09-15)

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](https://en.wikipedia.org/wiki/Entscheidungsproblem).

But In my AI course, we learned of an algorithm to prove or disprove new statements using the axioms known as [Resolution by refutation](http://athena.ecs.csus.edu/~logicp/unification-resolution/resolution-refutation.html). 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?

**Tags:** automated-theorem-proving, resolution


---

## 0 answers

