title: How does a Resolution algorithm work for propositional logic?
body: <p>I haven't been able to understand what the resolution rule is in propositional logic. Does resolution simply state some rules by which a sentence can be expanded and written in another form?<br>
  Following is a simple resolution algorithm for propositional logic. The function returns the set of all possible clauses obtained by resolving it's 2 input. I can't understand the working of the algorithm, could someone explain it to me? </p>
  
  <pre><code>  function PL-RESOLUTION(KB,α) returns true or false
       inputs: KB, the knowledge base, a sentence α in propositional logic, the query, a
               sentence in propositional logic 
       clauses &lt;--- the set of clauses in the CNF representation of KB ∧ ¬α
       new &lt;--- {}
       loop do
          for each Ci, Cj in clauses do
              resolvents &lt;----- PL-RESOLVE(Ci, Cj)
              if resolvents contains the empty clause then return true
              new &lt;--- new ∪ resolvents
          if new ⊆ clauses then return false
          clauses &lt;---- clauses  ∪ new                                                                           
  </code></pre>