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:
R = {((A B) A) B }.
Modus ponens.
Implicatie Eliminatie regel, '> el'.
Bewijs via resolutie:

Aanname van het tegendeel S:


S ≡ R;
S = {(((A B) A) B) }.

Normaal vorm conversies:


  · Negatief normaal vorm;
  · Conjunctief normaal vorm:
{((A B) A) B };
{(A B) A B }.
  · Clausule Normaal Vorm:
{ 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:.
Sluit (in contradictie).
Formule S is beslist onvervulbaar.
Formule R is resolutie-beslisbaar geldig.


Bewijs via resolutie (in PPL).



Gegeven formule R:
R = {((A B) (C D)) ((A C) (B D))}.
Bewijs via resolutie:

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)) };
{ ((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), }.

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:.
Sluit (in contradictie).
Formule S is beslist onvervulbaar.
Formule R is resolutie-beslisbaar geldig.


Bewijs via resolutie (in PPL).



Gegeven formule R:
R = {(((A C) (A B)) (C A)) (C B)}.
Bewijs via resolutie:

Aanname van het tegendeel S:


S ≡ R;
S = {(((A C) (A B)) (C A)) (C B)}.

Normaal vorm conversies:


  · 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), }.

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:.
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:
R ={ (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)))) )}.

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)))) };
  · 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)) };

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:
R = { (x A(x,x)) (y z A(y,z)) }.

Aanname van het tegendeel S:


S ≡ R;
S = { ( (x A(x,x)) (y z A(y,z)) ) }.

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));
(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.