Iti0210lab72 resolve

Resolve on funktsioon, mille sisend on disjunktid C1 ja C2 ning väljundiks kõik võimalikud resolutsioonireegli rakendamise tulemused sellele. Kuna uusi disjunkte saab tekkida mitu, siis väljund peaks olema list.

Näide 1:

 C1 = a v b
 C2 = a v -b

Tulemus:

 a

Näide 2:

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

Tulemus:

 a v b

Näide 3:

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

Tulemused (list), muuseas on mõlemad tautoloogiad ehk alati tõesed:

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

Näide 4:

 C1 = d
 C2 = -d

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