[subject]/[topic]

Az informatika logikai alapjaikövetkezik

Mi jön ezután?

A tárgy hátralévő témái a tematika szerint: konjunktív és diszjunktív normálforma, prenex alak és a szekvent kalkulus.

Forrás: a tárgy tematikája

A tárgy leírása szerint ezek következnek:

Normálformák

A diszjunktív normálforma (DNF) „vagyok és-ekből”, a konjunktív normálforma (KNF) „és-ek vagyokból” álló formula. Minden formula átalakítható mindkettőre, a nevezetes ekvivalenciák ismételt alkalmazásával:

  1. Fejezd ki a ⊃\supset és ≡\equiv jeleket: A⊃B⇔¬A∨BA \supset B \Leftrightarrow \neg A \vee B.
  2. Vidd be a tagadásokat az atomokig (De Morgan, kettős tagadás).
  3. Disztributivitással rendezd a kívánt alakra.
Példa

p⊃(q∧r)p \supset (q \wedge r)

  • DNF: ¬p∨(q∧r)\neg p \vee (q \wedge r)
  • KNF: (¬p∨q)∧(¬p∨r)(\neg p \vee q) \wedge (\neg p \vee r) (disztributivitás)

Ellenőrizd az ekvivalencia-tesztben, hogy a három alak ugyanaz!

Prenex alak

Elsőrendű formulánál az összes kvantort a formula elejére hozzuk: Q1x1…Qnxn BQ_1 x_1 \dots Q_n x_n\, B, ahol BB-ben nincs kvantor. Ehhez a kvantoros törvényeket és a kötött változók átnevezését használjuk.

Szekvent kalkulus

A következményt eddig szemantikusan (interpretációkkal, igazságtáblával) vizsgáltuk. A Gentzen-féle szekvent kalkulus szintaktikus módszer: szabályok alapján, jelsorozatok átírásával vezetünk le formulákat, interpretáció nélkül.