1
$\begingroup$

I'm searching for an authoritative definition of resolution (logic resolution).

Preferably on a reference freely available on the Internet (so I can read it right now).

If this is too broad then resolution for first order logic.

Thank you.

$\endgroup$

closed as off-topic by Yuval Filmus, Andrej Bauer, Sasho Nikolov, Vijay D, Jeffε Aug 14 '13 at 11:34

This question appears to be off-topic. The users who voted to close gave this specific reason:

If this question can be reworded to fit the rules in the help center, please edit the question.

  • 2
    $\begingroup$ Too basic for this site. $\endgroup$ – Yuval Filmus Aug 8 '13 at 19:10
  • 3
    $\begingroup$ Try googling "resolution proof system". $\endgroup$ – Yuval Filmus Aug 8 '13 at 19:11
  • 1
    $\begingroup$ @YuvalFilmus I think you didn't understand the question, please let me know any detail that may not be clear. Thank you. $\endgroup$ – Trylks Aug 9 '13 at 10:31
  • 1
    $\begingroup$ @Trylks, he wikipedia articles for resolution en.wikipedia.org/wiki/Resolution_(logic) and inference rules explain all these topics. Do you want a definition of resolution or to know whether it has certain properties? Your context does not help because both statements about resolution are vague. I don't understand the focus on "new theorems". $\endgroup$ – Vijay D Aug 10 '13 at 0:23
  • 1
    $\begingroup$ See also this discussion: cstheory.stackexchange.com/questions/16572/… $\endgroup$ – Vijay D Aug 10 '13 at 0:26
7
$\begingroup$

Unlike the question you threaten for inference rule, this has a nice, simple answer:

Robinson (1965) A machine-oriented logic based on the resolution principle. Journal of the ACM.

Resolution only applies to a subfragment of FOL, the Horn clauses, that lack disjunction and existential quantification, but combined with Herbrandisation, this is sufficient to encode satisfiability in the following sense: for any formula of FOL, we can find a Horn clause such that each is satisfiable if the other is.

Resolution is related to cut-elimination, but is more efficient.

Extending resolution to the whole of FOL requires a more sophistcated approach to unification than Robinson's algorithm. Uniform provability offers a technique for reading off such a computational mechanism from a cleaned-up proof theory of intuitionistic logic, higher-order unification, and the double-negation translation.

$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.