# 3. Übungsblatt

## Gruppe

Name:
Name:
Name:

## Übung 3.1: Resolution 


F =  { ~P \/ ~R, R \/ P, ~Q \/ P, ~Q \/ R, ~P \/ R }


... (Hier die Resolution)

## Hinweise

Markdown-Notation für Resolutionsbeweise: 

| Iteration |  Nummer | Klausel | Elternklauseln und Resolutionsliteral|
|---|----|----------------|-----|
| 0 |  1 | [A, B]         |     |
|   |  2 | [A, not(B), C] |     | 
| 1 | 3  | [A, C]         | Res 1,2 mit B|


Vereinfachte Markdown-Notation:  
- TT für Verum, FF für Falsum  
-  ~ für Negation  
- &, |, -->, <-> für die Konjunktion, Disjunktion, Implikation, Biimplikation  
- = für semantische Äquivalenz (≈)  

Alternativ könnt ihr auch Unicode verwenden: ⊥, ⊤, ¬, ∧, ∨, →, ↔, ≈