The use of resolution on ground clauses. A finite refutation ends in the empty ground clause and establishes unsatisfiability of the chosen ground instances. Herbrand's theorem explains the completeness of searching for such refutations for universal equality-free first-order clauses.
Articles by others on the same topic
There are currently no matching articles.