Iti0210lab72 resolve

Pl-Resolve on funktsioon, mille sisend on disjunktid C1 ja C2 ning väljundiks kõik võimalikud resolutsioonireegli rakendamise tulemused sellele. Väljund on list uutest disjunktidest.

Näide 1:

 C1 = a v b
 C2 = a v -b

Tulemused (list):

 a

Näide 2:

 C1 = a v b v -c v d
 C2 = a v c v -d

Tulemused (list):

 a v b v d v -d
 a v b v c v -c

Näide 3:

 C1 = d
 C2 = -d

Tulemus: tühi disjunkt. See tähendab ühtlasi, et leti vastuolu kogu teadmusbaasis (d & -d).