02 Kalküle

Introduction

Ableitungen der Form $F⊢G$

Oder: $\{F_1,\dots ,F_k\}⊢G$

Ableitung

${⊢}_R$ soll $\models$ imitieren nach festen Regeln R $F{⊢}_{R}G$ z.B. $\{F,G\}{⊢}_R(F\wedge G)$

• Schrittweise mehr Formeln aus einer Menge $M$ von gegebenen Formeln ableiten
• Kalkül ist eine (endliche) Menge von Regeln.

Schreibweise

$M{⊢}_{K}F$

Eigenschaften

Sound (man kann nur Wahres ableiten) $M{⊢}_{K}F⟹M\models F$

Vollständig (Completeness): $M\models F⟹M{⊢}_{K}F$

Beispiele für Sound

$\{F,\neg F\}{⊢}_{R}G$ (die LHS ist immer falsch, also gilt die logische Implikation immer) $\{F\vee G,\neg G\}{⊢}_{R}F\vee H$ $\varnothing {⊢}_R(F\to G)\vee (G\to F)$

Resolutionskalkül

Clause

A clause is a set of literals.

Quick-Facts

• Ziel: leere Menge herleiten, somit gezeigt, dass Formel unerfüllbar
• $\text{F ist unerfu¨llbar}⟺K(F){⊢}_{\text{res}}\varnothing$
• Resolutionskalkül ist korrekt

Aufgabe – Beweise dass F unerfüllbar ist

1. Bringe F in CNF
2. Wandle $F_{\text{CNF}}$ in Mengen um (jede Klausel ist eine Menge)
3. Resolutionsschritt so lange ausführen bis wir $\{\}$ hergeleitet haben

Logische Folgerung zeigen