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

<blockquote>
  <p>Robinson (1965) A machine-oriented logic based on the resolution principle. <em>Journal of the ACM</em>.</p>
</blockquote>

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

<p>Resolution is related to cut-elimination, but is more efficient.</p>

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

CC BY-SA 3.0
2013-08-09T18:57:48.503Z
2013-08-09T18:57:48.503Z
Charles Stewart
<p>I'm searching for an <strong>authoritative definition</strong> of resolution (logic resolution).</p>

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

<p>If this is too broad then resolution for first order logic.</p>

<p>Thank you.</p>

CC BY-SA 3.0
2013-08-08T19:10:17.850Z
Too basic for this site.
Yuval Filmus
CC BY-SA 3.0
2013-08-08T19:11:42.573Z
Try googling "resolution proof system".
Yuval Filmus
CC BY-SA 3.0
2013-08-09T10:31:21.377Z
@YuvalFilmus I think you didn't understand the question, please let me know any detail that may not be clear. Thank you.
Trylks
CC BY-SA 3.0
2013-08-10T00:23:24.503Z
@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
CC BY-SA 3.0
2013-08-10T00:26:30.673Z
See also this discussion: http://cstheory.stackexchange.com/questions/16572/is-propositional-resolution-a-complete-proof-system?rq=1
Vijay D
<lo.logic><resolution>
What is resolution ((in FOL))?
Trylks
# What is resolution ((in FOL))?

(Asked by: username_0 on 2013-08-08)

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.

**Tags:** lo.logic, resolution
> **Comments:**
> **username_1**: Too basic for this site.  
> **username_1**: Try googling "resolution proof system".  
> **username_0**: @YuvalFilmus I think you didn't understand the question, please let me know any detail that may not be clear. Thank you.  
> **username_2**: @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".  
> **username_2**: See also this discussion: http://cstheory.stackexchange.com/questions/16572/is-propositional-resolution-a-complete-proof-system?rq=1  

---

## 1 answers

### Answer by username_3 on 2013-08-09. Score: 7 | Accepted answer

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.


---

