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, fd( y))} (degres
)(v) A( x, fd( 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:=dd];
(degres)(cj.rdc.:inst.) A( x, dd) : geldig.
[ ref {(x1,d1),(x2,d1), ..};]
[ ref {((x1,x2, ..),d1)};]
[2a2] ·[ x:=dd];
(degres)(cj.rdc.:inst.) A( dd, dd
) [ref {(d1,d1)};]
: geldig.
[2a3] ·[ dd:= ds
]; (degres)(dj.xpn.:Sk+1) A( d
s, ds)
[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, gs(
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, gs( 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] ·[ gs( x, x)
:=hs( x)]; (syn.rdc.:Sk±1,snn.)
C_( x, hs( 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( cs, y)}
[ ref {((x1/x2/ ..).c0,y1), ((x1/x2/ ..).c0,y2), ..};]
[ ref {((x1/x2/ ..).c0,(y1,y2, ..)) ..};]
[2a] Route 1.
[2a1] ·[ y:=ds
]; (degres)(cj.-dj.rdc.) A( c
s, cs)
[ref {((x1,x1)/(x2,x2)/ ..).c0};]
: geldig.
[2b] Route 2 (ongeldige uitkomst):
[2b1] ·[ y:=dd];
(degres)(cj.rdc.:inst.) A( cs, d
d) : geldig.
[ ref {(x1,d1)/(x2,d1)/ ..};]
[ ref {((x1/x2/ ..),d1)};]
[2b2] ·[ dd:=d
s]; (degres)(dj.xpn.:Sk+1)
A( cs, ds)
[ref {((x1/x2/ ..).c0,(y1/y2/ ..).d0))};]
: geldig.
[2b3] ·[ ds:=
cs]; (degres)
(dj.rdc.) A( cs, cs)
[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, gs(
x))} [ref {(x1,(y1/y2/ ..).1),
(x2,(y1/y2/ ..).2), ..};]
[2a] Route 1.
[2a1] ·[( x, gs( x))
:= ( gs( x), gs( x
))]; (degres)(cj.-dj.rdc.:ssm.) A( g
s( x), gs( x)));
[ref {((y1/y2/ ..).1,(y1/y2/ ..).1),
((y1/y2/ ..).2,(y1/y2/ ..).2), ..};] : geldig.
[2a2] ·[ x:=cd];
(degres)(cj.rdc.:inst.) A( gs( c
d), gs( cd))
[ref {(y1/y2/ ..).c1,(y1/y2/ ..).c1};]
: geldig.
[2a3] Syntactische reductie:
·[ gs( cd
) :=cs]; (syn.rdc.:Sk±1,snn.)
A( cs, cs)
[ref {(y1/y2/ ..).c0,(y1/y2/ ..).c0};]
: geldig.
[2b] Route 2 (ongeldige uitkomst):
[2b1] ·[ x:=cd];
(degres)(cj.rdc.:inst.) A( cd, g
s( cd))
[ref {(c1,(y1/y2/ ..).c1)};]
: geldig.
[2b2] Syntactische reductie:
·[ gs( cd
) :=ds]; (Sk+1)
A( cd, ds) : geldig.
[ ref {((c1,y1)/(c1,y2)/ ..).d0};]
[ ref {(c1,(y1/y2/ ..).d0)};]
[2b3] ·[ cd:=c
s]; (degres)(dj.xpn.:Sk+1)
A( cs, ds) : geldig.
[ ref {(x1,y1)/(x1,y2)/ ..(x2,y1)/(x2,y2)/ ..};]
[ ref {(x1,(y1/y2/ ..).1)/ (x2,(y1/y2/ ..).2)/ ..};]
Maar (vervolg afleiding, ongeldig):
[2b4] ·[ ds:=
cs]; (degres)
(dj.rdc.;dj.xpn.) (A( ds, ds)
[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( cs, d
s)}
[ ref {(x1,(y1/y2/ ..).1)/ (x2,(y1/y2/ ..).2)/ ..};]
[ ref {(x1,y1)/(x1,y2)/ .. (x2,y1)/(x2,y2)/ ..};]
·[ ds:=cs
]; (degres)(dj.rdc.) A( c
s, cs)
[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.
|
|