Strom lineárního vstupního (LI)-rezolučního odvození ◻ z P ⋃ {G}, kde P je množina Hornových klauzulí a G cílová klauzule, je vždy zároveň stromem

lineárního rezolučního vyvrácení P ⋃ {G}

LD-rezolučního odvození ◻ z P ⋃ {¬G}

lineárního rezolučního odvození G z P

Predchádzajúca

Ďalšia

Vymazať štatistiky

Zle zodpovedané otázky: