Skip to main content

Unification/Resolution: Set-based

Describe Resolution as set-based search model

Model​

alt text alt text

Process​

fwert​

  1. always choose Factorization first
  2. next do Resolution based on size

alt text

fselect​

use alphabetical order to tie break alt text

Example​

alt text

Remember x and y in each clause (line) are different

alt text

No factorization → Resolution apply alt text alt text alt text alt text