Formele-logica-predikatenlogica-PDL-bewijs-resolutie-voorbeelden

**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 }.

Modus ponens. Implicatie Eliminatie regel, '> el'.
Bewijs via resolutie.

•

Aanname van het tegendeel S.

S ≡ ¬R;

S = {¬(((A

B) }.

•

Normaal vorm conversies.

· Negatief normaal vorm;
· Conjunctief normaal vorm.

{((A

¬B };

{(¬A

¬B }.

· Clausule Normaal vorm.

{ 1:A, 2:¬B, 3:(¬A

B) }.

•

Reductie(s).

Pad (a).
{1,3}

4:B; {2,4}

.
Pad (b).
{1,3}

4:¬A; {1,4}

Sluit (in contradictie).

Formule S is beslist onvervulbaar.

Formule R is resolutie-beslisbaar geldig.

Bewijs via resolutie (in PPL).

Gegeven formule R.

R = {((A

D))

((A

D))}.

Bewijs via resolutie.

•

Aanname van het tegendeel S.

S ≡ ¬R;

S = { ¬(((A

D))

((A

D))) }.

•

Normaal vorm conversies.

· Negatief normaal vorm.

{ ((A

D))

¬((A

D)) };

{ ((A

D))

((A

¬(B

D)) };

· Conjunctief normaal vorm.

{ ((¬A

(¬C

D))

((A

(¬B

¬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}

.
Pad (b).
{2,5}

8:D; {4,8}

10:¬B; {1,3}

6:B; {6,10}

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)

B))

A))

B)}.

Bewijs via resolutie.

•

Aanname van het tegendeel S.

S ≡ ¬R;

S = {¬(((A

¬C)

B))

A))

B)}.

•

Normaal vorm conversies.

· Negatief normaal vorm.

{(((A

¬C)

B))

A))

¬(C

B)};

{(((A

¬C)

B))

A))

¬B)};

· Conjunctief normaal vorm.

{(((¬A

¬C)

(¬A

B))

(¬C

A))

¬B)};

{(¬A

¬C

¬A

(¬C

¬B)};

{(¬A

¬C)

(¬B

C)};

· Clausule Normaal vorm.

{ 1:¬B, 2:C 3:(A

¬C), 4:(¬A

¬C), }.

•

Reductie(s).

Pad (a).
{2,3}

5:A; {1,4}

6:(¬A

¬C); {5,6}

7:¬C; {2,7}

.
Pad (b).
{2,4}

9:(¬A

B); {1,9}

10:¬A; {2,3}

7:¬C; {3,12}

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))

(

z A(y,z)) }.

•

Aanname van het tegendeel S.

S ≡ ¬R;

S = { ¬( (

x A(x,x))

(

z A(y,z)) ) }.

•

Normaal vorm conversies.

· Negatief normaal vorm (1).

{ (

x A(x,x))

¬(

z A(y,z)) ) }.

· Conjunctief normaal vorm.
· Kwantor prefix vorm.

{ (

x A(x,x))

(

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.


*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.