|
|
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 PPLVoorbeelden van validiteitsbewijs in PPL via Resolutie.Bewijs via resolutie (in PPL).
Gegeven formule R.
R = {((A B) A)
B }.
Modus ponens.
Implicatie Eliminatie regel, '> el'.Bewijs via resolutie.
•
Formule R is resolutie-beslisbaar geldig.Aanname van het tegendeel S.
S ≡ ¬R;
S = {¬(((A B) A) B) }.
•
Formule S is beslist onvervulbaar.Normaal vorm conversies.· Negatief normaal vorm; · Conjunctief normaal vorm.
{((A B) A)
¬B };
· Clausule Normaal vorm.
{(¬A B) A ¬B }.
{ 1:A, 2:¬B, 3:(¬A B) }.
•
Sluit (in contradictie).
Reductie(s).
Pad (a).
{1,3} 4:B; {2,4} 5: . Pad (b). {1,3} 4:¬A; {1,4} 5: . Bewijs via resolutie (in PPL).
Gegeven formule R.
R = {((A B) (C
D)) ((A C) (B
D))}.
Bewijs via resolutie.
•
Formule R is resolutie-beslisbaar geldig.Aanname van het tegendeel S.
S ≡ ¬R;
S = { ¬(((A B) (C D)) ((A C) (B D))) }.
•
Normaal vorm conversies.· Negatief normaal vorm.
{ ((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.
{ (¬A B) (¬C D) A C (¬B ¬D) }.
{ 1:A, 2:C, 3:(¬A B), 4:(¬B
¬D) 5:(¬C D), }.
•
Formule S is beslist onvervulbaar.Reductie(s).
Pad (a).
Sluit (in contradictie).
{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: . Bewijs via resolutie (in PPL).
Gegeven formule R.
R = {(((A ¬C) (A
B)) (C A))
(C B)}.
Bewijs via resolutie.
•
Formule R is resolutie-beslisbaar geldig.Aanname van het tegendeel S.
S ≡ ¬R;
S = {¬(((A ¬C) (A B)) (C A)) (C B)}.
•
Formule S is beslist onvervulbaar.Normaal vorm conversies.· Negatief normaal vorm.
{(((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)};
· Clausule Normaal vorm.
{(¬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), }.
•
Reductie(s).
Pad (a).
Sluit (in contradictie).
{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: . Resolutie in PDLVoorbeelden van validiteitsbewijs in PDL via Resolutie.Bewijs via resolutie (in PDL-I).
Gegeven formule R.
Formule R is resolutie-beslisbaar geldig.Conversie DNV naar CNV.
R ={ (x ((A(x) B(x))
C(x)))
((x (A(x) C(x))) (y (B(y) C(y)))) }.
•
Formule S is beslisbaar onvervulbaar.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)))) )}.
•
Normaal vorm conversies.· Negatief normaal vorm.
{ (x ((A(x) B(x))
C(x)))
· Skolem Normaal vorm.
¬((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))))
· Conjunctief normaal vorm.
( (¬A(c) ¬C(c)) (¬B(d) ¬C(d))) }; Kwantor prefix vorm.
{ (x ((A(x) C(x))
(B(x) C(x))))
· Universele Instantie vorm.
((¬A(c) ¬B(d)) (¬A(c) ¬C(d))) ((¬C(c) ¬B(d)) (¬C(c) ¬C(d))) };
{ ((A(x) C(x))
(B(x) C(x)))
· Clausule Normaal vorm.
((¬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)) };
•
Variabelen-herbenoeming(en),Unificatie(s),Reductie(s).
(1) {1·[x:=c]} 7:(A(c)
C(c));
Syntactische contradictie.{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. Voorbeeld van onbeslisbare stelling in PDL-I.
Gegeven formule R.
R = { (x A(x,x)) (
y z A(y,z)) }.
•
Formule R is niet resolutie-beslisbaar geldig.Aanname van het tegendeel S.
S ≡ ¬R;
S = { ¬( (x A(x,x)) (y z A(y,z)) ) }.
•
Formule S is niet beslisbaar onvervulbaar.Normaal vorm conversies.· 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)) }.
•
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));
Oneindige circulariteit.(2) C2[x:=f(y)]; C2:A(f(y)),f(f(y))); .. etc.. |
|