Methode 'Praktische Logica':
Bewijsmethode voor Formele logica
.Voorbeelden van bewijzen via de Resolutiemethode.
Bewijs via resolutie.
Voorbeelden van logische bewijsreeksen via Resolutie.
Resolutie-deductiereeksen.
{Zie voor uitleg:
Inleiding Resolutielogica.
Resolutie in PPL
Voorbeelden van validiteitsbewijs in PPL via Resolutie.
Bewijs via resolutie (in PPL).
Gegeven formule R.
Bewijs via resolutie.
Formule R is resolutie-beslisbaar geldig.
R = {((A 
B) 
A)
B }.
Modus ponens. Implicatie Eliminatie regel, '> el'. B) A)
B }.Bewijs via resolutie.
•
S ≡ ¬R;
S = {¬(((A B) A)
B) }.
Formule S is beslist onvervulbaar.
Aanname van het tegendeel S.
S ≡ ¬R;
S = {¬(((A B) A)
B) }.
•
· Negatief normaal vorm;
· Conjunctief normaal vorm.
{((A B) A)
¬B };
{(¬A 
B) A
¬B }.
· Clausule Normaal vorm.
{ 1:A, 2:¬B, 3:(¬A B) }.
Sluit (in contradictie).
Normaal vorm conversies.
· Negatief normaal vorm;
· Conjunctief normaal vorm.
{((A B) A)
¬B };
{(¬A B) A
¬B }.
{ 1:A, 2:¬B, 3:(¬A B) }.
•
Reductie(s).
Pad (a).
{1,3} 4:B; {2,4}
5: 
.
Pad (b).
{1,3} 4:¬A; {1,4}
5: .
{1,3}
4:B; {2,4}
5: .Pad (b).
{1,3}
4:¬A; {1,4}
5: .
Sluit (in contradictie).
Formule S is beslist onvervulbaar.
Formule R is resolutie-beslisbaar geldig.Bewijs via resolutie (in PPL).
Gegeven formule R.
Formule R is resolutie-beslisbaar geldig.
R = {((A B) (C
D))
((A C)
(B D))}.
Bewijs via resolutie. B) (C
D))
((A C)
(B D))}.
•
S ≡ ¬R;
S = { ¬(((A B) (C
D)) ((A
C) (B
D))) }.
Formule S is beslist onvervulbaar.
Aanname van het tegendeel S.
S ≡ ¬R;
S = { ¬(((A B) (C
D)) ((A
C) (B
D))) }.
•
· Negatief normaal vorm.
{ ((A B) (C
D)) ¬((A
C) (B
D)) };
{ ((A B)
(C D)) ((A
C) ¬(B
D)) };
· Conjunctief normaal vorm.
{ ((¬A B)
(¬C D)) ((A
C) (¬B
¬D)) };
{ (¬A B) (¬C
D) A
C (¬B
¬D) }.
· Clausule Normaal vorm.
{ 1:A, 2:C, 3:(¬A B), 4:(¬B ¬D) 5:(¬C D), }.
Normaal vorm conversies.
· Negatief normaal vorm.
{ ((A B) (C
D)) ¬((A
C) (B
D)) };
{ ((A B)
(C D)) ((A
C) ¬(B
D)) };
{ ((¬A B)
(¬C D)) ((A
C) (¬B
¬D)) };
{ (¬A B) (¬C
D) A
C (¬B
¬D) }.
{ 1:A, 2:C, 3:(¬A B), 4:(¬B ¬D) 5:(¬C D), }.
•
Sluit (in contradictie).
Reductie(s).
Pad (a).
{1,3} 6:B; {4,6} 7:¬D; {2,5}
8:D; {7,8}
9: .
Pad (b).
{2,5} 8:D; {4,8} 10:¬B; {1,3}
6:B; {6,10}
9: .
{1,3}
6:B; {4,6} 7:¬D; {2,5}
8:D; {7,8}
9: .Pad (b).
{2,5}
8:D; {4,8} 10:¬B; {1,3}
6:B; {6,10}
9: .
Sluit (in contradictie).
Formule S is beslist onvervulbaar.
Formule R is resolutie-beslisbaar geldig.Bewijs via resolutie (in PPL).
Gegeven formule R.
Formule R is resolutie-beslisbaar geldig.
R = {(((A ¬C) (A
B)) (C
A)) (C
B)}.
Bewijs via resolutie. ¬C) (A
B)) (C
A)) (C
B)}.
•
S ≡ ¬R;
S = {¬(((A ¬C) (A
B)) (C
A)) (C
B)}.
Formule S is beslist onvervulbaar.
Aanname van het tegendeel S.
S ≡ ¬R;
S = {¬(((A ¬C) (A
B)) (C
A)) (C
B)}.
•
· Negatief normaal vorm.
{(((A ¬C) (A
B)) (C
A)) ¬(C
B)};
{(((A ¬C) (A
B)) (C
A)) (C
¬B)};
· Conjunctief normaal vorm.
{(((¬A ¬C) (¬A
B)) (¬C
A)) (C
¬B)};
{(¬A ¬C ¬A
B) (¬C
A) (C
¬B)};
{(¬A B ¬C)
(A ¬C)
(¬B C)};
· Clausule Normaal vorm.
{ 1:¬B, 2:C 3:(A ¬C), 4:(¬A B
¬C), }.
Normaal vorm conversies.
· Negatief normaal vorm.
{(((A ¬C) (A
B)) (C
A)) ¬(C
B)};
{(((A ¬C) (A
B)) (C
A)) (C
¬B)};
{(((¬A ¬C) (¬A
B)) (¬C
A)) (C
¬B)};
{(¬A ¬C ¬A
B) (¬C
A) (C
¬B)};
{(¬A B ¬C)
(A ¬C)
(¬B C)};
{ 1:¬B, 2:C 3:(A ¬C), 4:(¬A B
¬C), }.
•
Sluit (in contradictie).
Reductie(s).
Pad (a).
{2,3} 5:A; {1,4}
6:(¬A ¬C); {5,6} 7:¬C; {2,7}
8: .
Pad (b).
{2,4}
9:(¬A B); {1,9} 10:¬A; {2,3}
7:¬C; {3,12}
8: .
{2,3}
5:A; {1,4}
6:(¬A ¬C); {5,6} 7:¬C; {2,7}
8: .Pad (b).
{2,4}
9:(¬A B); {1,9} 10:¬A; {2,3}
7:¬C; {3,12}
8: .
Sluit (in contradictie).
Formule S is beslist onvervulbaar.
Formule R is resolutie-beslisbaar geldig.Resolutie in PDL
Voorbeelden van validiteitsbewijs in PDL via Resolutie.
Bewijs via resolutie (in PDL-I).
Gegeven formule R.
Conversie DNV naar CNV.
Formule S is beslisbaar onvervulbaar.
Conversie DNV naar CNV.
R ={ (
x ((A(x) B(x))
C(x)))
((x (A(x) C(x)))
(y (B(y) C(y)))) }.
x ((A(x) B(x))
C(x)))
((x (A(x) C(x)))
(y (B(y) C(y)))) }.
•
S ≡ ¬R;
S = {¬( (x ((A(x) B(x))
C(x)))
((x (A(x) C(x)))
(y (B(y) C(y)))) )}.
Aanname van het tegendeel S.
S ≡ ¬R;
S = {¬( (x ((A(x) B(x))
C(x)))
((x (A(x) C(x)))
(y (B(y) C(y)))) )}.
•
· Negatief normaal vorm.
{ (x ((A(x) B(x))
C(x)))
¬((x (A(x) C(x)))
(y (B(y) C(y)))) };
{ (x ((A(x) B(x))
C(x)))
(¬(x (A(x) C(x)))
¬(y (B(y) C(y)))) };
{ (x ((A(x) B(x))
C(x)))
( (
x ¬(A(x) C(x)))
(y ¬(B(y) C(y)))) };
{ (x ((A(x) B(x))
C(x)))
( (x (¬A(x) ¬C(x)))
(y (¬B(y) ¬C(y)))) };
{ (x ((A(x) B(x))
C(x)))
( (x (¬A(x) ¬C(x)))
(y (¬B(y) ¬C(y)))) };
· Skolem Normaal vorm.
{ (x ((A(x) C(x))
(B(x) C(x))))
( (¬A(c) ¬C(c))
(¬B(d) ¬C(d))) };
· Conjunctief normaal vorm.
Kwantor prefix vorm.
{ (x ((A(x) C(x))
(B(x) C(x))))
((¬A(c) ¬B(d))
(¬A(c) ¬C(d)))
((¬C(c) ¬B(d))
(¬C(c) ¬C(d))) };
· Universele Instantie vorm.
{ ((A(x) C(x))
(B(x) C(x)))
((¬A(c) ¬B(d))
(¬A(c) ¬C(d)))
((¬C(c) ¬B(d))
(¬C(c) ¬C(d))) };
· Clausule Normaal vorm.
{ 1:(A(x) C(x)), 2:(B(x) C(x)),
3:(¬A(c) ¬B(d)), 4:(¬A(c)
¬C(d)),
5:(¬C(c) ¬B(d)), 6:(¬C(c)
¬C(d)) };
Normaal vorm conversies.
· Negatief normaal vorm.
{ (x ((A(x) B(x))
C(x)))
¬((x (A(x) C(x)))
(y (B(y) C(y)))) };
{ (x ((A(x) B(x))
C(x)))
(¬(x (A(x) C(x)))
¬(y (B(y) C(y)))) };
{ (x ((A(x) B(x))
C(x)))
( (x ¬(A(x) C(x)))
(y ¬(B(y) C(y)))) };
{ (x ((A(x) B(x))
C(x)))
( (x (¬A(x) ¬C(x)))
(y (¬B(y) ¬C(y)))) };
{ (x ((A(x) B(x))
C(x)))
( (x (¬A(x) ¬C(x)))
(y (¬B(y) ¬C(y)))) };
{ (x ((A(x) C(x))
(B(x) C(x))))
( (¬A(c) ¬C(c))
(¬B(d) ¬C(d))) };Kwantor prefix vorm.
{ (x ((A(x) C(x))
(B(x) C(x))))
((¬A(c) ¬B(d))
(¬A(c) ¬C(d)))
((¬C(c) ¬B(d))
(¬C(c) ¬C(d))) };
{ ((A(x) C(x))
(B(x) C(x)))
((¬A(c) ¬B(d))
(¬A(c) ¬C(d)))
((¬C(c) ¬B(d))
(¬C(c) ¬C(d))) };
{ 1:(A(x) C(x)), 2:(B(x) C(x)),3:(¬A(c)
¬B(d)), 4:(¬A(c)
¬C(d)),5:(¬C(c)
¬B(d)), 6:(¬C(c)
¬C(d)) };
•
(1) {1·[x:=c]}
7:(A(c) C(c));
{4,7} 8:(C(c) ¬C(d));
{6,8} 9:(¬C(d) ¬C(d));
{9} 10:¬C(d);
(2) {2·[y:=d]} 11:(B(d) C(d));
{10,11} 12:B(d);
{3,12} 13:¬A(c);
{5,7} 14:(A(c) ¬B(d));
{12,14} 15:A(c);
{13,15}
16:
: sluit.
Syntactische contradictie.
Variabelen-herbenoeming(en),
Unificatie(s),
Reductie(s).
(1) {1·[x:=c]}
7:(A(c) C(c));{4,7}
8:(C(c) ¬C(d));{6,8}
9:(¬C(d) ¬C(d));{9}
10:¬C(d);(2) {2·[y:=d]}
11:(B(d) C(d));{10,11}
12:B(d);{3,12}
13:¬A(c);{5,7}
14:(A(c) ¬B(d));{12,14}
15:A(c);{13,15}
16:
: sluit.
Syntactische contradictie.
Formule S is beslisbaar onvervulbaar.
Formule R is resolutie-beslisbaar geldig.Voorbeeld van onbeslisbare stelling in PDL-I.
Gegeven formule R.
Formule R is niet resolutie-beslisbaar geldig.
R = { (x A(x,x))
(y z A(y,z)) }.
x A(x,x))
(y z A(y,z)) }.
•
S ≡ ¬R;
S = { ¬( (x A(x,x))
(y z A(y,z)) ) }.
Formule S is niet beslisbaar onvervulbaar.
Aanname van het tegendeel S.
S ≡ ¬R;
S = { ¬( (x A(x,x))
(y z A(y,z)) ) }.
•
· Negatief normaal vorm (1).
{ (x A(x,x))
¬(y z A(y,z)) ) }.
· Conjunctief normaal vorm.
· Kwantor prefix vorm.
{ (x A(x,x))
(y z ¬A(y,z)) };
· Skolem Normaal vorm.
{ (x A(x,x))
(y ¬A(y,f(y))) };
· Universele Instantie vorm.
{ A(x,x))
¬A(y,f(y)) };
· Clausule Normaal vorm.
{ 1:A(x,x), 2:¬A(y,f(y)) }.
Normaal vorm conversies.
· Negatief normaal vorm (1).
{ (x A(x,x))
¬(y z A(y,z)) ) }.· Kwantor prefix vorm.
{ (x A(x,x))
(y z ¬A(y,z)) };
{ (x A(x,x))
(y ¬A(y,f(y))) };
{ A(x,x))
¬A(y,f(y)) };
{ 1:A(x,x), 2:¬A(y,f(y)) }.
•
{ C1:A(x,x), C2:¬A(y,f(y)) ·[y:=x] };
{ C1:A(x,x), C2:A(x,f(x)) };
Oneindige circulariteit.
Variabelen-herbenoeming(en),
Unificatie(s),
Reductie(s).
{ C1:A(x,x), C2:¬A(y,f(y)) ·[y:=x] };
{ C1:A(x,x), C2:A(x,f(x)) };
(1)
C1[x:=f(y)];
C1:A(f(y),f(y));
(2)
C2[x:=f(y)];
C2:A(f(y)),f(f(y))); .. etc..
C1[x:=f(y)];
C1:A(f(y),f(y));(2)
C2[x:=f(y)];
C2:A(f(y)),f(f(y))); .. etc..
Oneindige circulariteit.
Formule S is niet beslisbaar onvervulbaar.
Formule R is niet resolutie-beslisbaar geldig.