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.