Iti0210lab72 resolve: erinevus redaktsioonide vahel
Mine navigeerimisribale
Mine otsikasti
Uus lehekülg: '''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 di...' |
Resümee puudub |
||
| 1. rida: | 1. rida: | ||
'' | ''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: | '''Näide 1''': | ||
C1 = a v b | C1 = a v b | ||
C2 = a v -b | C2 = a v -b | ||
Tulemus: | |||
a | a | ||
Näide 2: | '''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 | C1 = a v b v -c v d | ||
C2 = a v c v -d | C2 = a v c v -d | ||
Tulemused (list): | Tulemused (list), muuseas on mõlemad tautoloogiad ehk alati tõesed: | ||
a v b v d v -d | a v b v d v -d | ||
a v b v c v -c | a v b v c v -c | ||
Näide | '''Näide 4''': | ||
C1 = d | C1 = d | ||
Redaktsioon: 9. märts 2020, kell 11:29
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).