algoritmus na opt. unifikator je takyto priblizne?
- k=0 0 opisat fi1 fi2 fiX najst Dk { v com sa lisia formuly }
- k=1 { nejaka z Dk / nejaka z Dk + subst. ovplyvni predch. AlfaK }, ficka so substituovanymi vecami, Dk { zase v com sa lisia }
- az kym sa ficka nerovnaju
ak mam Dk { x, y, z }, je jedno ci substituujem x/y alebo y/x ?