1

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.

Trylks
  • 604
  • 4
  • 9
  • 2
    Too basic for this site. – Yuval Filmus Aug 08 '13 at 19:10
  • 3
    Try googling "resolution proof system". – Yuval Filmus Aug 08 '13 at 19:11
  • 1
    @YuvalFilmus I think you didn't understand the question, please let me know any detail that may not be clear. Thank you. – Trylks Aug 09 '13 at 10:31
  • 1
    @Trylks, he wikipedia articles for resolution http://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". – Vijay D Aug 10 '13 at 00:23
  • 1
    See also this discussion: http://cstheory.stackexchange.com/questions/16572/is-propositional-resolution-a-complete-proof-system?rq=1 – Vijay D Aug 10 '13 at 00:26

1 Answers1

7

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.

Charles Stewart
  • 4,316
  • 28
  • 45