Øv med flashcards — Inferens i utsagnslogikk

Kapittel 12 · TDT4136

1 / 27

← Tilbake til kapittelet

27 kort

Formel

Resolusjonsregelen

Formel

\frac{ℓ _{1} \lor \dots \lor ℓ _{k} , m _{1} \lor \dots \lor m _{n}}{alle ℓ og m unntatt ℓ _{i} og m _{j}} der ℓ_{i} = \neg m_{j}

Brukes i hvert resolusjonssteg. Resolver på nøyaktig ett komplementært par om gangen; har to klausuler to par, gir hvert av dem en tautologi, aldri □.

Tips: bruk piltastene for å bla og mellomrom/Enter for å snu kortet.