Strom LD-rezolučního odvození ◻ z P ⋃ {G}, kde P je množina Hornových klauzulí a G cílová klazule, je vždy zároveň stromem

LD-rezolučního vyvrácení P ⋃ {G}

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

Lineárního vstupního (LI)-rezolučního odvození G z P

Predchádzajúca

Ďalšia

Vymazať štatistiky

Zle zodpovedané otázky: