Logické odvozování s výrazy

Logické odvozování s pomocí logických výrazů je formální varianta odvozování logických důsledků slovy.

Jde o proces, kdy dostaneme několik logických výrazů (faktů) a odvozujeme z nich jiný výraz (závěr). Nemusíme ale nutně jen odvozovat nové závěry, můžeme se i například pokoušet rozhodnout, jestli nějaký dodaný výrok plyne z jiných.

Říkáme, že výraz se dá odvodit (tedy vyplývá) ze zadaných výrazů právě tehdy, když platí ve všech případech, kdy platí všechny zadané výrazy.

Příklady

• Z výrazu X \text{ and } Y můžeme odvodit X, protože kdykoli platí X \text{ and } Y, musí platit X i Y, a tím spíš musí platit i samotné X.
• Z výrazů X \text{ or } Y a \text{not } X můžeme odvodit Y. Aby bylo splněno X \text{ or } Y, musí platit X nebo Y, ale X platit nemůže. Proto platí Y.
• Z výrazů X \Leftrightarrow Y a X můžeme odvodit Y. Výraz X \Leftrightarrow Y říká, že Y má vždy stejnou hodnotu jako X. Z pravdivosti X tak můžeme odvodit pravdivost Y.