AL0PFX1.htm

Cursus / training:

Methode Formele Logica

©

VI.

 

Deductieregels: Regels voor transformatie onder parafrase en/of degressie .



GELDIG/ ONGELDIG.



14.

 

Argument-unificatie/ Kwantor-samenvoeging (QJ), geldig - vanuit term.



14.1.

 

Regels voor Argument-unificatie; via Kwantor reductie, Substitutie, en/of Subsumptie .



Unificatie: Identiek maken van twee expressies (tekenreeksen).
Bewerkstelligen van congruentie d.i. uniformiteit van (minstens) twee expressies.

Unificatie in

PDL

.


Bewerkstelligen van congruentie d.i. uniformiteit van de argumentlijsten van predikaties met dezelfde predikaatnamen.
Door het zoeken van een gemeenschappelijk referentiegebied in het betreffende domein.
Via tactische argument-reductie/ instantiatie; van argument-variabelen.
Wordt bereikt via minstens één substitutie van één term c.q. argument door een andere.
Er moet op zijn minst een niet-leeg intersectiegebied zijn tussen de referentiegebieden van de termen.

Unificatie gebeurt via hetzij (a) variabele-hernoeming, renaming oftewel permutatie (P); hetzij (b) argument-reductie/ instantiatie.
(a) Een variabele-permutatie (P) is geldig onder parafrase of degressie.
Zie 11.2 (4.1).
(b) Een (specificerende) argument-reductie/ instantiatie (I), is altijd uitsluitend geldig onder degressie .
Zie 11.2 (4.2).

In feite is een unificerende substitutie-operatie een 'ad hoc' interpretatie van variabele argumenten.
Ze kan leiden tot syntactische doublure, en daardoor indirect tot eliminatie van expressies, m.n. literalen.

14.1.1.

 

Algemene basisregels voor unificatie.



Notaties.


'

=

(u)' : congruentie (doublure) onder argumenten-unificatie.
'≡(u)' : Equivalentie onder argumenten-unificatie.
'(u)' : Implicatie onder argumenten-unificatie.

(1)

Regels voor unificatie via renaming.


(1a) Regel t.b.v. unificatie van termen/ predicaat-argumenten, via renaming.
{x y ((x

=

y )  (h z (

t

[h]·[z

:=

x]

=

(v )

t

[h]·[z

:=

y] )z,h ) )y,x }.
(1b) Regel voor unificatie van predicaties/ literalen, via renaming.
{x y ((x

=

y )  (h z (F[h]·[z

:=

x] ≡(v) F [h]·[z

:=

y] )z,h) )y ,x }.

(2)

Regels t.b.v. unificatie argument-reductie/ instantiatie.


(2a) Regel t.b.v. unificatie van termen/ predicaat-argumenten, via instantiatie.
{i j ((

R

*(

t

[j])

R

*(

t

[i]))  (h k (

R

*(

t

[h]·[

t

[k]

:=

t

[j]]

R

*(

t

[h]·[

t

[k]

:=

t

[i]] )k,h) )j,i }.
(3b) Regel t.b.v. unificatie van predicaties/ literalen, via instantiatie.
{i j ((

R

*(

t

[j])

R

*(

t

[i]))  (h k (F[h]·[

t

[k]

:=

t

[i]]  (

degres

)
(i) F [h]·[

t

[k]

:=

t

[j] ] )k,h) )j,i }.

14.1.2.

 

Regels voor unificatie, o.a. t.b.v. reductie, o.a. in resolutie.



Gebruikte verkortingen:


L1: Literaal, antecedens.
L2: Literaal, consequens.

C1: Clause, antecedens.
C2: Clause, consequens.

Vuistregel(s):


• Behoud in het substraat maximaal referentieel bereik (generaliteit).
• Beperk de mogelijke toename van over-all nesting-diepte (term complexiteit).

Most General Unifier (MGU):


een unificatie-operatie met maximaal behoud van referentieel bereik (generaliteit) van de predicaat-argumenten.
MGU instantiatie: een instantiatie die tot MGU unificatie van expressies leidt.
{i j ((

R

*(

t

[i],

t

[j])

=

{

R

*(

t

[i]),

R

*(

t

[j])} );
(k (

R

*(

t

[k])

R

*(

t

[i ],

t

[j]) );
(

|

R

*(

t

[i] ,

t

[j])

|

|

R

*(

t

[k])

|

> 0 ) );
 (h m ((G[m]

=

{F[h](

t

[i]), F[ h](

t

[j])} ·[

t

[i]

:=

t

[k];

t

[j]

:=

t

[ k]] );
 (G[m]  (u) F [h](

t

[k]) );
((

R

*(

t

[k])

=

R

*(

t

[i],

t

[j]) )   (G[m]  (mgu) F[h](

t

[k]) ) ) )m) )h) )k) )j, i }.

14.2.

 

Vormen van U-/ E- kwantor samenvoeging

(

QJU

/

QJE

).

Argument-unificatie/ Kwantor-samenvoeging: Universeel, Existentieel.

Toepasbaar in Literaal, Conjunctie, Disjunctie.

14.2.1.

 

Argument-unificatie/ Kwantor-samenvoeging; Binnen één Literaal.



(a1a)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabelen, meervoudig, naar variabele .


Via hernoeming (renaming).

(a1a-1):
Bijv.: {x y A(x,y)}   ·[y

:=

x];   (

degres

)
(cj.rdc.) (x A(x,x)) : geldig .
 (Skl.) {A(x,y)}
 [

ref

{(x1,(y1,y2, ..)1)/ (x2,(y1,y2, ..).2)/ ..};]
 [

ref

{(x1,y1),(x1,y2), ..(x2,y1),(x2,y2), ..};]
  ·[y

:=

x];   (

degres

)
(cj.rdc.:ren.) A(x,x)
 [

ref

{(x1,x1),(x2,x2), ..};]
: geldig.
Zo ook:
Bijv.: {A(x,

f

d(y))}  (

degres

)
(v) A(x,

f

d(x)) : geldig.

(a1b)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig, naar 'Skolem' constante.



(a1b-1):
Bijv.: {x y A(x,y)}   ·[y

:=

x];   (

degres

)
(cj.rdc.;dj.xpn.) (x A(x,x )) : geldig.
 (Skl.) [1] {A(x,y)}  [

ref

{(x1,y1),(x1,y2), ..(x2,y1),(x2,y2), ..};]

[2a] Route 1.
[2a1]   ·[y

:=

d

d];   (

degres

)
(cj.rdc.:inst.) A(x,

d

d) : geldig.
 [

ref

{(x1,d1),(x2,d1), ..};]
 [

ref

{((x1,x2, ..),d1)};]
[2a2]   ·[x

:=

d

d];   (

degres

)
(cj.rdc.:inst.) A(

d

d,

d

d )  [

ref

{(d1,d1)};]
: geldig.
[2a3]  ·[

d

d:=

d

s

];  (

degres

)
(dj.xpn.:Sk+1) A(

d

s

,

d

s

)
 [

ref

{(x1,x1)/(x2,x2)/ ..};]
: geldig.

(a2a)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig, naar 'Skolem' functie.



(a2a-1):
Bijv.: {x w y C_(w,y)}   ·[w

:=

x];   (cj.rdc.) (x y C_(x,y))) : geldig.
 (Skl.) [1] {C_(w,

g

s

( x,w))}
 [

ref

{(w1,(y1/y2/..).x1.w1), (w1,(y1/y2/..).x2.w1), ..
(w2,(y1/y2/..).x1.w2), (w2,(y1/y2/..).x2.w2), ..};]

(D.w.z. steeds een nieuwe, onbepaalde keuze uit y, per uniek paar (x,w)).
Conjunctieve reductie:
[2]   ·[w

:=

x];   (

degres

)
(cj.rdc.) C_(x,

g

s

(x ,x) )
 [

ref

{(x1,(y1/y2/..).x1.x1), (x2,(y1/y2/..).x2.x2), ..};]
: geldig.
(D.w.z. steeds een nieuwe, onbepaalde keuze uit y, per uniek paar (x,x), c.q. element x.
Syntactische reductie (synonymie):
[3]  ·[

g

s

(x,x)

:=

h

s

(x)];  (syn.rdc.:Sk±1,snn.) C_(x,

h

s

(x) )
 [

ref

{(x1,(y1/y2/..).x1), (x2,(y1/y2/..).x2), ..};]
: geldig.
(D.w.z. steeds een nieuwe, onbepaalde keuze uit y, per uniek element x.

(a2b)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig, via 'Skolem' functie.



(a2b-1):
Bijv.: {x y A(x,y)}   (

degres

)
(cj.rdc.;dj.xpn.) ( x A(x,x)) : geldig.
 (Skl.) [1] {A(

c

s

,y)}
 [

ref

{((x1/x2/ ..).c0,y1), ((x1/x2/ ..).c0,y2), ..};]
 [

ref

{((x1/x2/ ..).c0,(y1,y2, ..)) ..};]
[2a] Route 1.
[2a1]  ·[y

:=

d

s

];  (

degres

)
(cj.-dj.rdc.) A(

c

s

,

c

s

)
 [

ref

{((x1,x1)/(x2,x2)/ ..).c0};]
: geldig.

[2b] Route 2 (ongeldige uitkomst):
[2b1]  ·[y

:=

d

d];   (

degres

)
(cj.rdc.:inst.) A(

c

s

,

d

d) : geldig.
 [

ref

{(x1,d1)/(x2,d1)/ ..};]
 [

ref

{((x1/x2/ ..),d1)};]
[2b2]  ·[

d

d

:=

d

s

];  (

degres

)
(dj.xpn.:Sk+1) A(

c

s

,

d

s

)
 [

ref

{((x1/x2/ ..).c0,(y1/y2/ ..).d0))};]
: geldig.
[2b3]  ·[

d

s

:=

c

s

];  (

degres

)
(dj.rdc.) A(

c

s

,

c

s

)
 [

ref

{((x1,x1)/(x2,x2)/ ..).c0};]
:

ongeldig

.

(a3)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig, naar 'Skolem' constanten.


Verschillende Skolem constanten in dezelfde argumentenlijst van een predicatie (enkelvoudige formule, Literaal) verwijzen naar onafhankelijke selecties.

Niet unificeerbaar is '', d.i. y-afhankelijkheid van x;
met ongepaarde variabelen, bijv. (x,y).
(a3-1):
Bijv.: {x y A(x,y)}   (

degres

)
(cj.rdc.;dj.xpn.;dj.rdc.) ( y A(y,y)) : geldig.
 (Skl.) [1] {A(x,

g

s

( x))}  [

ref

{(x1,(y1/y2/ ..).1), (x2,(y1/y2/ ..).2), ..};]

[2a] Route 1.
[2a1]  ·[(x,

g

s

(x))

:=

(

g

s

(x),

g

s

(x ))];  (

degres

)
(cj.-dj.rdc.:ssm.) A(

g

s

(x),

g

s

(x)));
 [

ref

{((y1/y2/ ..).1,(y1/y2/ ..).1), ((y1/y2/ ..).2,(y1/y2/ ..).2), ..};]
: geldig.
[2a2]  ·[x

:=

c

d];   (

degres

)
(cj.rdc.:inst.) A(

g

s

(

c

d),

g

s

(

c

d))
 [

ref

{(y1/y2/ ..).c1,(y1/y2/ ..).c1};]
: geldig.
[2a3] Syntactische reductie:
 ·[

g

s

(

c

d )

:=

c

s

];  (syn.rdc.:Sk±1,snn.) A(

c

s

,

c

s

)
 [

ref

{(y1/y2/ ..).c0,(y1/y2/ ..).c0};]
: geldig.

[2b] Route 2 (ongeldige uitkomst):
[2b1]  ·[x

:=

c

d];   (

degres

)
(cj.rdc.:inst.) A(

c

d,

g

s

(

c

d))
 [

ref

{(c1,(y1/y2/ ..).c1)};]
: geldig.
[2b2] Syntactische reductie:
 ·[

g

s

(

c

d )

:=

d

s

];  (Sk+1) A(

c

d,

d

s

) : geldig.
 [

ref

{((c1,y1)/(c1,y2)/ ..).d0};]
 [

ref

{(c1,(y1/y2/ ..).d0)};]
[2b3]  ·[

c

d

:=

c

s

];  (

degres

)
(dj.xpn.:Sk+1) A(

c

s

,

d

s

) : geldig.
 [

ref

{(x1,y1)/(x1,y2)/ ..(x2,y1)/(x2,y2)/ ..};]
 [

ref

{(x1,(y1/y2/ ..).1)/ (x2,(y1/y2/ ..).2)/ ..};]
Maar (vervolg afleiding, ongeldig):
[2b4]  ·[

d

s

:=

c

s

];  (

degres

)
(dj.rdc.;dj.xpn.) (A(

d

s

,

d

s

)
 [

ref

{(y1,y1)/(y2,y2)/ ..};]
:

ongeldig

.

Niet unificeerbaar is '', met ongepaarde variabele n, bijv. (x,y).
(a3-2):
Bijv.: {x y A(x,y)}   ·[y

:=

x];   (

degres

)
(dj.rdc.) (x A(x,x)) :

ongeldig

.
 (Skl.) {A(

c

s

,

d

s

)}
 [

ref

{(x1,(y1/y2/ ..).1)/ (x2,(y1/y2/ ..).2)/ ..};]  [

ref

{(x1,y1)/(x1,y2)/ .. (x2,y1)/(x2,y2)/ ..};]
  ·[

d

s

:=

c

s ];  (

degres

)
(dj.rdc.) A(

c

s

,

c

s

)
 [

ref

{(x1,x1)/(x2,x2)/ ..};]
:

ongeldig

.

14.2.2.

 

Argument-unificatie/ Kwantor-samenvoeging ; In Conjunctie.




14.2.3.

 

Argument-unificatie/ Kwantor-samenvoeging ; In Disjunctie.




C.P. van der Velde © 2004, 2016, 2019.