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.