B. Baumgarten – Aussagenlogik
Ein einfaches Beispiel für Resolution
B. Baumgarten – Aussagenlogik
Ist diese Formel erfüllbar?
(¬A → B)∧ (A → ¬B)∧ (¬A → ¬B)∧ (A → B)
B. Baumgarten – Aussagenlogik
Ist diese Formel erfüllbar?
(¬A → B)∧ (A → ¬B)∧ (¬A → ¬B)∧ (A → B)
syntaktische Umformung in KNF:
B. Baumgarten – Aussagenlogik
Ist diese Formel erfüllbar?
(¬A → B)∧ (A → ¬B)∧ (¬A → ¬B)∧ (A → B)
syntaktische Umformung in KNF,
erste vier Schritte (ϕ→ψ
¬ϕ∨ψ):
B. Baumgarten – Aussagenlogik
Ist diese Formel erfüllbar?
(¬A → B)∧ (A → ¬B)∧ (¬A → ¬B)∧ (A → B)
syntaktische Umformung in KNF,
erste vier Schritte (ϕ→ψ
¬ϕ∨ψ):
(¬¬A ∨ B)∧ (¬A ∨ ¬B)∧ (¬¬A ∨ ¬B)∧ (¬A ∨ B)
B. Baumgarten – Aussagenlogik
Ist diese Formel erfüllbar?
(¬A → B)∧ (A → ¬B)∧ (¬A → ¬B)∧ (A → B)
syntaktische Umformung in KNF,
erste vier Schritte (ϕ→ψ
¬ϕ∨ψ):
(¬¬A ∨ B)∧ (¬A ∨ ¬B)∧ (¬¬A ∨ ¬B)∧ (¬A ∨ B)
zwei Schritte (¬¬ϕ
ϕ):
B. Baumgarten – Aussagenlogik
Ist diese Formel erfüllbar?
(¬A → B)∧ (A → ¬B)∧ (¬A → ¬B)∧ (A → B)
syntaktische Umformung in KNF,
erste vier Schritte (ϕ→ψ
¬ϕ∨ψ):
(¬¬A ∨ B)∧ (¬A ∨ ¬B)∧ (¬¬A ∨ ¬B)∧ (¬A ∨ B)
zwei Schritte (¬¬ϕ
ϕ):
(A ∨ B)∧ (¬A ∨ ¬B)∧ (A ∨ ¬B)∧ (¬A ∨ B)
B. Baumgarten – Aussagenlogik
Ist diese Formel erfüllbar?
(¬A → B)∧ (A → ¬B)∧ (¬A → ¬B)∧ (A → B)
syntaktische Umformung in KNF,
erste vier Schritte (ϕ→ψ
¬ϕ∨ψ):
(¬¬A ∨ B)∧ (¬A ∨ ¬B)∧ (¬¬A ∨ ¬B)∧ (¬A ∨ B)
zwei Schritte (¬¬ϕ
ϕ):
(A ∨ B)∧ (¬A ∨ ¬B)∧ (A ∨ ¬B)∧ (¬A ∨ B)
Resolution mit
A,B
¬A , ¬B
A , ¬B
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A , ¬B
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A , ¬B
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A , ¬B
A
¬A
∅
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A , ¬B
A
¬A
∅
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A , ¬B
A
¬A , B
¬A
∅
Es folgt:
(A ∨ B)∧ (¬A ∨ ¬B)∧ (A ∨ ¬B)∧ (¬A ∨ B)
und damit
(¬A → B)∧ (A → ¬B)∧ (¬A → ¬B)∧ (A → B)
sind unerfüllbar.
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A , ¬B
A
¬A , B
¬A
∅
Wegen der freien Auswahl des jeweils nächsten Schrittes
sind andere Abläufe möglich:
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
¬B
A , ¬B
¬A
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
¬B
A , ¬B
¬A
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
¬B
A , ¬B
¬A
B
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
¬B
A , ¬B
¬A
B
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A
B
¬B
∅
¬A , B
B. Baumgarten – Aussagenlogik
Resolution
A,B
¬A , ¬B
A
A , ¬B
¬A
B
¬B
∅
¬A , B