Resolutionsalgorithmus

Es gibt vier Arten von Klauseln.

A :- B1 , B2 , B3 steht für (B1 und B2 und B3) -> A, also (¬B1 oder ¬B2 oder ¬B3) oder A

A :- steht für wahr -> A, also A

:- B1 , B2 , B3 steht für (B1 und B2 und B3) -> falsch , also (¬B1 oder ¬B2 oder ¬B3)

:- steht für wahr -> falsch , also falsch

Ziel ist es, eine Anfrage :- B1 , B2 , B3 in :- umzuformen.

Beispiel 1:

Als Beispiel dient ein Syllogismus der alten Griechen.

Alle Menschen sind sterblich
Sokrates ist ein Mensch
Sokrates ist sterblich

In unserem Resolutionsalg. sehen die ersten beiden Zeilen so aus:

P:
Sterblich(x) :- Mensch(x)
Mensch(Sokrates) :-

Die Anfrage hat die Form

Γ:
:- Sterblich(Sokrates)

Die erste Klausel ist eine Regel und besagt Mensch(x) -> Sterblich(x).
Das ist gleichbedeutend mit ¬ Mensch(x) V Sterblich(x).

Die zweite Klausel ist ein Faktum und besagt w -> Mensch(Sokrates)

Die Anfrage bedeutet ¬ Sterblich(Sokrates).

Also wird die Behauptung negiert, um einen Widerspruch zu erzeugen. Wird der Widerspruch erzeugt, so ist die Behauptung bewiesen. Dafür muss die Klausel

:-

hergeleitet werden.

Ablauf:

Γ = :- Sterblich(Sokrates)
α = Sterblich(x) :- Mensch(x)
ω = [ x / Sokrates ]
Γ' = :- Mensch(Sokrates)
α = Mensch(Sokrates)
ω = [ ]
ω' = [ x / Sokrates ]
Γ' = :-

Erfolg. Sokrates ist sterblich.

Diese Berechnung drückt umgangssprachlich folgende Überlegung aus:

Annahme: ¬ Sterblich(Sokrates).
Wegen Mensch(x) -> Sterblich(x) folgt Mensch(Sokrates) -> Sterblich(Sokrates). Daraus folgt ¬ Mensch(Sokrates).
Wegen Mensch(Sokrates) folgt Widerspruch.

Beispiel 2:

Als Beispiel dienen Verwandschaftsgrade.

Kind(Ludwig, Karl)
Verheiratet(Berta , Karl)
(Kind(x,y) und Verheiratet( y, z)) -> Kind( x, z)
Verheiratet(x,y) -> Verheiratet(y,x)
Kind(Ludwig, Berta)

In unserem Resolutionsalg. sehen die ersten vier Zeilen so aus:

P:
Kind(Ludwig, Karl) :-
Verheiratet(Berta, Karl) :-
Kind( x, z) :- Kind(x,y) , Verheiratet( y, z)
Verheiratet(x, y) :- Verheiratet(y, x)

Die Anfrage hat die Form

Γ:
:- Kind(Ludwig, Berta)

Ablauf:

Γ = :- Kind(Ludwig, Berta)
α = Kind( x, z) :- Kind(x,y) , Verheiratet( y, z)
ω = [ x / Ludwig, z/Berta]
Γ' = :- Kind(Ludwig,y) , Verheiratet( y, Berta)
α = Kind(Ludwig, Karl) :-
ω = [ y/Karl ]
ω' = [ x / Ludwig, z/Berta , y/Karl ]
Γ' = :- Verheiratet( Karl, Berta)
α = Verheiratet(x', y') :- Verheiratet(y', x')
ω = [ x'/Karl , y'/Berta]
ω' = [ x / Ludwig, z/Berta , y/Karl , x'/Karl , y'/Berta]
Γ' = :- Verheiratet( Berta , Karl )
α = Verheiratet( Berta , Karl ) :-
ω = [ ]
ω' = [ x / Ludwig, z/Berta , y/Karl , x'/Karl , y'/Berta]
Γ' = :-

Die Abfrage wird positiv beantwortet.

Beispiel 3:

Als Beispiel dienen Verwandschaftsgrade.

In unserem Resolutionsalg. sehen die ersten vier Zeilen so aus:

P:
Kind(Ludwig, Karl) :-
Verheiratet(Berta, Karl) :-
Kind( x, z) :- Kind(x,y) , Verheiratet( y, z)
Verheiratet(x, y) :- Verheiratet(y, x)

Die Anfrage hat die Form

Γ:
:- Kind(Ludwig, z)

Ablauf 1:

Γ = :- Kind(Ludwig, z)
α = Kind( x, z) :- Kind(x,y) , Verheiratet( y, z)
ω = [ x / Ludwig ]
Γ' = :- Kind(Ludwig,y) , Verheiratet( y, z)
α = Kind(Ludwig, Karl) :-
ω = [ y/Karl ]
ω' = [ x / Ludwig, z/Berta , y/Karl ]
Γ' = :- Verheiratet( Karl, Berta)
α = Verheiratet(x', y') :- Verheiratet(y', x')
ω = [ x'/Karl , y'/Berta]
ω' = [ x / Ludwig, z/Berta , y/Karl , x'/Karl , y'/Berta]
Γ' = :- Verheiratet( Berta , Karl )
α = Verheiratet( Berta , Karl ) :-
ω = [ ]
ω' = [ x / Ludwig, z/Berta , y/Karl , x'/Karl , y'/Berta]
Γ' = :-

Die Abfrage wird positiv beantwortet.