Introductie_Predikatenlogica_PDL_Deel_VI_H_14-14_2

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.

{

y ((x

=

y )

(

z (

t

_[h]·[z

:=

=

_(v)

t

_[h]·[z

:=

y] )_z,_h) )_y,_x }.

(1b) Regel voor unificatie van predicaties/ literalen, via renaming.

{

y ((x

=

y )

(

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.

{

j ((

R

^*(

t

_[j])

R

^*(

t

_[i]))

(

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.

{

j ((

R

^*(

t

_[j])

R

^*(

t

_[i]))

(

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.

{

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

(

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.: {

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.: {

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

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

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

[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.: {

y C_(w,y)}

·[w

:=

x];

_(cj.rdc.) (

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.: {

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

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

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

[2b2]

·[

d

:=

d

_s];

_(degres
)_{(dj.xpn.:Sk+1)} A(

c

_s,

d

_s)
[

_ref {((x1/x2/ ..).c0,(y1/y2/ ..).d0))};] : geldig.

[2b3]

·[

d

:=

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.: {

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

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

_ref {(c1,(y1/y2/ ..).d0)};] : geldig.

[2b3]

·[

c

:=

c

_s];

_(degres
)_{(dj.xpn.:Sk+1)} A(

c

_s,

d

_s)
[

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

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

Maar (vervolg afleiding, ongeldig):
[2b4]

·[

d

:=

c

_s];

_(degres)_{(dj.rdc.;dj.xpn.)} (A(

d

_s,

d

_s)
[

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

ongeldig

Niet unificeerbaar is '

', met ongepaarde variabelen, bijv. (x,y).
(a3-2):

Bijv.: {

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

:=

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.

[*ZIE: AL3LQ14N_CJ1.htm :]

14.2.3. Argument-unificatie/ Kwantor-samenvoeging; In Disjunctie.

[*ZIE: AL3LQ14N_DJ1.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 in PDL.

PDL

14.1.1.

Algemene basisregels voor unificatie.

Notaties.

=

Regels voor unificatie via renaming.

=

t

:=

=

t

:=

=

:=

:=

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

R

t

R

t

R

t

t

:=

t

R

t

t

:=

t

R

t

R

t

t

:=

t

degres

t

:=

t

14.1.2.

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

Gebruikte verkortingen:

Vuistregel(s):

Most General Unifier (MGU):

R

t

t

=

R

t

R

t

R

t

R

t

t

|

R

t

t

|

|

R

t

|

=

^©

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

Unificatie in
PDL
.

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