Cursus / training: Methode Formele Logica
©
V. Wetten voor logische Normaal Vorm conversies [II].
Syntactische verkorting.
7.
Parafrase reductie via Syntactische doublure eliminatie.
Suboptimale (overcomplete) logische syntax.
Syntactische redundantie - vanwege directe syntactische identiteit (syntactische, 'letterlijke' doublure(s)
, replicatie, reïteratie).
Dat wil zeggen: 'letterlijke' herhaling van elementen in hetzelfde verband (d.i. de directe context: nesting, inbedding, ..).
Regels voor eliminatie van doublure(s), duplicaten, 'klonen'.
7A.
Directe Syntactische doublure.
(Directe) Identiteit (impliceert Equivalentie/ Parafrase)).
(·) Basale of lokale, enkelvoudige of complexe equivalentie, van literalen en/of subformules
(onder unificatie).
7A.1.
Directe Syntactische doublure, in Conjunctie.
(7A.1a) Eenvoudige/ algemene vorm.
Elimineren van redundante conjuncte; op grond van ' Basale equivalentie' (onder unificatie).
Bijv.: {A  A} [ (A 
A);] (u) A.
Idem, in Parallelle Negatie).
Bijv.: {A \ A} [(¬A ¬A);]
(u) ¬A.
(7A.1b) (Directe) Complexe equivalentie); in Conjunctie.
Betreft equivalentie van meerdere (complexe) disjuncties.
Elimineren van redundante (complexe) disjunctie; op grond van ' Complexe equivalentie'.
Bijv.: {(A  B) (A B)
C} (2u) ((A
B) C).
Bijv.: {(A B C) (A
B C) D}
(3u) ((A B C)
C).
7A.2. Directe Syntactische doublure
, in Disjunctie.
(7A.2a) Eenvoudige/ algemene vorm.
Elimineren van redundante disjunct; op grond van ' Basale equivalentie' (onder unificatie).
Principe: 'Propositional reduction rule', 'P-reduction'.
N(r) : operator van gereduceerde clauses verkregen door p-reductie.
Reduct: 'P-reduct'.
Bijv.: {A A} [ (A
(u) A);] (u) A.
Bijv.: {A (A X)} [
(A A X);]
(u) (A X).
Idem, in Implicatie.
Voorwaardelijke premisse-regel.
Ketenredenering, reductie, keten-verkorting.
Bijv.: {A  (A B)}
[ (¬A (¬A B));
(¬A ¬A B);
(u) (¬A B);]
degres)(u) (A
B).
Idem, in Exclusie.
Bijv.: {A | A} [(¬A ¬A);]
(u) ¬A.
(7A.2b) (Directe) Complexe equivalentie); in Disjunctie.
Elimineren van redundante (complexe) conjunctie; op grond van ' Complexe equivalentie'.
Betreft equivalentie van meerdere (complexe) conjuncties.
Bijv.: {(A B) (A B)
C} (2u) ((A
B) C).
Bijv.: {(A B C) (A
B C) D}
(3u) ((A B C)
C).
7B. Indirecte Syntactische doublure
.
Indirecte Basale equivalentie, onder unificatie.
Levert ' Basale redundantie'.
Betreft relaties tussen unit clauses ( literalen op de hoofdlijn).
7B.1.
Indirecte Syntactische doublure, in Conjunctie.
Overtollige conjunct(en).
(Indirecte) Complexe equivalentie); in Conjunctie.
In Parallelle Negatie.
Bijv.: {(A \ A) \ (B \ B)}
[ (¬(A \ A) ¬(B \ B) );
(¬(¬A ¬A) ¬(¬B ¬B) );
(A A) (B
B) );]
(A B).
Bijv.: {(A \ B) \ (A \ B)}
[ (¬(A \ B) ¬(A \ B) );
(¬(¬A ¬B) ¬(¬A ¬B) );
(A B) (A
B) );]
(A B).
7B.2. Indirecte Syntactische doublure
, in Disjunctie.
Overtollige disjunct(en).
(7B.2a) (Indirecte) Complexe equivalentie; in Disjunctie.
In Exclusie.
Bijv.: {(A | X) | (A | X)}
[ (¬(A | X) ¬(A | X) );]
(¬(¬A ¬ X) ¬(¬A
¬ X) );] ((A X)
(A X) );]
(A X).
(7B.2b) Indirecte Basale equivalentie; in Disjunctie.
Directe Transferente equivalentie, bij een (geneste) afleidingsregel.
Niet uitkomend op Transferente contradictie:
Transferente equivalentie tussen disjuncte basale literaal en lokale conclusie binnen een
geneste afleidingsregel.
Pragmatiek /Consequenties:
Irrelevante basale literaal, die niet met enig effect toepasbaar is.
(7B.2c) Indirecte Basale equivalentie; In implicatie.
Contra-logische conclusie.
Conclusie is strijdig met uitgangspunten.
(7B.2c1) Contra-logische conclusie, algemene vorm.
(7B.2c2) Contra-logische conclusie, met conjuncte premissen.
8. Wetten voor Negatief Normaal Vorm
(NNF) conversie.
Alle geldig onder parafrase/ equivalentie.
8A.
Dubbele negatie-eliminatie.
Wet van de Dubbele Ontkenning ( Negatio duplex).
Negatie eliminatie regel ('¬ el').
(Frege axioma: 5).
O.a. bruikbaar voor Syntactische doublure reductie.
Bijv.: {¬¬A} ¬(¬A);
A.
(8A.1) 'Dubbele ontkenning (I)'; Duplex negatio affirmat.
Bijv.: {¬(¬A)} ¬¬A;
A.
(8A.2). 'Dubbele ontkenning (II)'.
: [Ht2] =(H2)
Bijv.: {  h1 k1 ( ('¬¬F [h1]
'  K *[k1])  ('F [
h1]' K *[k1]) ) h1,k1 }.
8B. Negatie-binnenplaatsing.
O.a. bruikbaar voor Connectief normaal vorm conversie ( Conjunctie/ Disjunctie).
(8B.1) Negatie-binnenplaatsing, op literaal.
Bijv.: {¬(A)} (¬A); ¬A.
, Consistentie: [Ht1] =(H1)
Bijv.: { k1 (K *[k1] 
WFF *( L![l1] ) )
(CONSIS(K *[k1] )
 h1 ( (F [h1]
ATM *( L![l1] ) )
(a) ( ('¬F [h1]' K *
[k1] ) (¬('F [h1]' K
*[k1] ) );
(b) ( ('F [h1]' K *
[k1] ) ('¬(¬F [h1]'
K *[k1] ) );
(c) ¬( ('F [h1]' K *
[k1] ) ('¬F [h1]' K
*[k1] ) ) ) h1 ) ) k1 }.
8C. Negatie-binnenplaatsing, op
relatie - met connectief-conversie, negatie-distributie.
D.i. Negatie-binnenplaatsing met Negatie Distributie ('Negatie spreiding').
(8C.1) Negatieve conjunctie omzetting (T3).
Negatief-conjunct-normaal conversie.
'Negatie spreiding', m.b.v. Wet van De Morgan ( De Morgan's Law), De Morgan's Theorema (1).
(8C.2) Negatieve disjunctie omzetting (T4).
Negatief-disjunct-normaal conversie.
'Negatie spreiding', m.b.v. Wet van De Morgan ( De Morgan's Laws), De Morgan's Theorema (2).
(8C.3) Negatieve implicatie omzetting.
(8C.4) Naar Conjunctie: Negatieve equivalentie
omzetting.
Bijv.: {¬(A ≡ B)} (A # B);
((A B) (¬A
¬B)).
(8C.5) Naar Disjunctie: Negatieve exclusief-disjunctie omzetting.
Bijv.: {¬(A # B)} (A
B); ((¬A B)
(A ¬B)).
VI. Wetten voor logische Normaal Vorm conversies [III].
9. Connectief Normaal Vorm conversie
.
Syntactische standaardisatie door connectief normaal vorm conversie.
O.a. Comprimatie, Distributie.
Alle geldig onder parafrase/ equivalentie.
In de vorige stap lieten we nog in het midden of de deelverzamelingen binnen de totale theorie onderling in een specifieke
logische relatie stonden: disjunctief of conjunctief.
Een handige vorm voor formules wanneer we ze willen beoordelen is de Connectief Normaal vorm ( Connective Normal form
).
De volgende regels betreffen standaardisatie van connectieven.
Normaal vorm conversie naar connectief levert de volgende voordelen.
(a) Maximale syntactische standaardisatie.
Door uniformering van het hoofdconnectief.
Dit bevordert directe vergelijkbaarheid van formules.
(b) Volledige volgorde-onafhankelijkheid. Door eliminatie van implicaties.
Dit dient eveneens directe vergelijkbaarheid, en daarnaast efficiënte verwerking.
(c) Minimale syntactische complexiteit, oftewel nestingdiepte.
Maximale reductie van syntactische complexiteit oftewel nestingdiepte.
Dit bevordert efficiënte verwerking.
Deze herformulering heeft vervolgens nog meer belangrijke voordelen.
(d) Volledig behoud van logische kracht.
De normaal vorm versie gebeurt onder parafrase, dus het resultaat is logisch semantisch gelijkwaardig
aan het origineel. Dat wil zeggen, ze bevat géén wijziging c.q. vermindering ( degressie) van logische kracht.
(e) Maximale congruentie met semantische resp. referentiële bewijsstructuur.
Als gevolg van deze normaal vorm conversie ligt de syntactische vorm van een formule of expressie zo dicht mogelijk bij
de semantische structuur van de weergegeven bewering of redenering.
Hierdoor ligt ze eveneens zo dicht mogelijk bij de bewijsstructuur, die uitsluitsel geeft over het gehalte van waarheid en geldigheid
van die bewering of redenering. Deze bewijsstructuur is onderdeel van de ' grondstructuur', oftewel de verzameling
objecttoestanden die aanwezig zijn in een bepaald buitenlogisch domein.
Hierdoor is deze structuur optimaal voor een toetsing en bewijsvoering (c.q. weerlegging) die maximaal accuraat en
efficiënt is.
{N.b. Uiteraard blijft onveranderd gelden dat de weergegeven logische relatie als zodanig buiten het referentieel
domein ligt. Dit is direct duidelijk in het geval van disjunctie. Daarmee hebben we een volgend bewijs voor
de onverenigbaarheid, onoverbrugbare discrepantie, asymmterie tussen logisch domein en andere domeinen, zoals
fysisch domein of mentaal domein.
Zie hierover ook: Concepten van informatie. Een analyse van de belangrijkste opvattingen van informatie.
}
Een formule in Connectief Normaal vorm maakt uitsluitend gebruik van een beperkt aantal connectieven: {¬,
, }.
Uitgangspunt is een eerste, algemene indeling van formules in twee basis- vormen overeenkomstig het hoofdconnectief
:
Conjunctief (hoofdconnectief) Vorm ( CJF),
en Disjunctief (hoofdconnectief) Vorm ( DJF).
Vervolgens hebben we de keuze tussen twee basis- normaalvormen:
Conjunct Normaal Vorm ( CNF),
en Disjunct Normaal Vorm ( DNF).
(1) Een formule in conjunctief normaal vorm (CNF):
Of multiplicatieve canonische vorm,
heeft de vorm van een conjunctie van literalen en/of van disjuncties van literalen.
Met andere woorden, op de hoofdlijn van redenering bestaat een nevenstelling van één of meer conjuncten, waarbij elke conjunct bestaat uit
een disjunctie samengesteld uit minstens één enkelvoudige formule (atoom of literaal).
Algemene structuur van een CNF verzameling:
(T * = WFF *( L!PDl));
( k ( (K *[k]
CNF *(T *))
(K *[k] = { [ F[1]
[ F[2] .. ] ] F[n[k]] } )
(n[k] = SIZE(K *[k]) )
(K *[k] = {  (j[k]=1,..n[
k]) F[j[k]] } )
( ( j ( ( F[j]
K *[k])
F[j] = { [ G[j,1]
[ G[j,2] .. G[m[j[k]]] ] ] } )
(m[j[k]] = SIZE( F[j])
( ( F[j] = {  (h[j[k]]=1,..h
[n[k]]) G[h[j[k]]]) } )
( (0 > j[k] ≥ n[k] ) (0 > h[j[k]] ≥
m[j[k]]) ) ) ) j ) k );
Toepassing:
Bekijken we een verzameling van formules als conjunctieve elementen, dan kunnen we onderzoeken of er een combinatie
van die elementen is die gezamenlijk kunnen dienen als een bepaalde (externe) theorie.
O.a. bruikbaar voor de Bewijsmethode van Resolutie.
(2) Een formule in disjunctief normaal vorm (DNF):
Of additieve canonische vorm,
heeft de vorm van een disjunctie van literalen en/of van conjuncties van literalen.
Met andere woorden, op de hoofdlijn van redenering bestaat een nevenstelling van één of meer disjuncten, waarbij elke disjunct bestaat uit
een conjunctie samengesteld uit minstens één enkelvoudige formule (atoom of literaal).
Algemene structuur van een DNF verzameling:
(T * = WFF *( L!PDl));
( k ( (K *[k]
CNF *(T *))
(K *[k] = { [ F[1]
[ F[2] .. ] ] F[n[k]] } )
(n[k] = SIZE(K *[k]) )
(K *[k] = { (j[k]=1,..n[
k]) F[j[k]] } )
( ( j ( ( F[j]
K *[k])
F[j] = { [ G[j,1]
[ G[j,2] .. G[m[j[k]]] ] ] } )
(m[j[k]] = SIZE( F[j])
( ( F[j] = { (h[j[k]]=1,..h
[n[k]]) G[h[j[k]]]) } )
( (0 > j[k] ≥ n[k] ) (0 > h[j[k]] ≥
m[j[k]]) ) ) ) j ) k );
Toepassing:
Bekijken we een verzameling van formules als disjunctieve elementen, dan kunnen we onderzoeken wèlke van die elementen
afzonderlijk kunnen dienen als voldoende premissen voor een bepaalde (externe) theorie.
O.a. bruikbaar voor de Bewijsmethode van Minimaal domein definitie.
9A.
Connectief conversie: naar Conjunctie.
Connectief-transformatie voor CNF conversie.
Omzetting van een formule naar een conjunctie van (disjuncties) van literalen.
Met name voor toetsing van bewering of conclusie(s).
(Kan indirect bij DNF conversie bruikbaar zijn).
Alle geldig onder parafrase/ equivalentie.
9A.1
Connectief conversie: naar Conjunctie, algemeen.
(9A.1a) Disjunctie Conjunctief omzetting.
(9A.1b) Implicatie Conjunctief omzetting.
9A.2 Connectief conversie, naar Conjunctief
normaal vorm (CNF); divers.
Connectief-transformatie voor CNF conversie, divers.
(9A.2a) Negatief-implicatie normaal omzetting.
Bijv.: {¬(A B)} (¬(¬A
B)); (A
¬B).
(9A.2b) Equivalentie Conjunctief omzetting.
(9A.2c) Exclusief-disjunctie Conjunctief omzetting.
Bijv.: {A # B} ((A
¬B) (B ¬A));
((¬A ¬B) (A B)).
9A.3 Connectief conversie, naar Conjunctie
; via Distributie.
Connectief-transformatie voor CNF conversie, via Distributie.
Expansie via verspreiden ( Distributie) van basale termen/ literalen.
Naar ( partiële) ' Symmetrische equivalentie' I, van geneste disjuncten.
(9A.3a) Distributie, naar Conjunctie.
Verspreiden ( Distributie) van basale disjunct.
Met toenemende nesting complexiteit:
(9A.3a.1) idem; Vanuit DNF, met atoom-diepte = 2.
Bijv.: {A (B C)};
(distr.) ((A B) (A
C)).
Bijv.: {(A B) (C D)};
[1e: hoofdconnectief (niveau 1) ' ' naar ' ':]
(distr.1) ((A B)
C)
((A B) D) );
[2e: genest connectief (niveau 2) ' ' naar ' ':]
(distr.2) (((A C)
(B C)) ((A D)
(B D)) );
((A C)
(A D) (B C)
(B D)).
Bijv.: {(A1 A2) (B1 B2)}
(distr.1) (((A1 A2)
B1) ((A1 A2) B2) );
(2xdistr.) ((A1 B1)
(A1 B2) (A2 B1)
(A2 B2) ).
Algemene structuur, in DNF:
{(A [1] .. A [n])
(B [1] .. B [m])};
(2xdistr.) {CNF: ((A [1] B
[1]) .. (A [1] B
[m])); .. ((A [n]
B [1]) .. (A [n] B [m]))}.
(9A.3a.2) Idem; Vanuit DNF, met atoom-diepte = 3.
Bijv.: {A
(B (C
D))};
[hoofdconnectief (niveau 1) ' ' naar ' ':]
(distr.1) ((A B)
(A (C D)) );
((A B)
(A C D)).
(9A.3a.3) Idem; Vanuit DNF, met atoom-diepte = 4.
Bijv.: {A (B (C
(D E)))};
[1st genest connectief (niveau 3) ' ' naar ' ':]
(distr.1) (A (B
((C D)
(D E))) );
[2st hoofdconnectief (niveau 1) ' ' naar ' ':]
(distr.2) ((A B)
(A ((C D) (D
E))) );
((A B) ((A
C D) (A D
E)) );
((A B)
(A C D) (A
D E)).
(9A.3b) Idem, in implicatie: Distributie, van conclusie(s).
(9A.3c) Idem, in implicatie: Distributie, van premisse(n).
9A.4 Connectief conversie: naar Conjunctie
, via Comprimatie.
Connectief-transformatie voor CNF conversie, via Comprimatie.
Reductie via samentrekken ( Contractie) van lokale termen/ literalen.
Wegens ( partiële) ' Symmetrische equivalentie' I, van geneste conjuncten.
Stap (1) Samentrekking (contractie) van disjuncte conjuncties,
op grond van minstens één gemeenschappelijke - parallel-equivalente - lokale conjunct.
Stap (2) Onttrekking (destillatie) van minstens twee parallel-equivalente lokale conjuncten, en transitie naar de hoofdlijn.
(9A.4a) Comprimatie, van lokale disjuncten naar basale conjunct.
(9A.4a.1) Idem; Vanuit DNF, met atoom-diepte = 2.
Bijv.: {(A1 B) (A1 C)}
(compr.)(u) (A1 (B
C) );
Bijv.: {(A1 B) (A1 A2)}
(compr.)(u) (A1 (A2
B) );
Niet verder reduceerbaar.
Tabelbewijs:.
(kolommen A1, A2, B):
Atc:
{(A1: $(1111.0000) B: $(1010.1010))
(A1: $(1111.0000) A2: $(1100.1100))};
( $(1010.0000) $(1100.0000));
$(1110.0000).
Csq:
{A1: $(1111.0000) (A2: $(1100.1100)
B: $(1010.1010))};
( $(1111.0000) $(1110.1110));
$(1110.0000) : geldig.
Bijv.: {(A1 B1) (A1
B2) (A2 B1) (A2
B2) }
(2xlok.compr.) ((A1 (B1
B2)) (A2 (B1 B2)) );
(nas.compr.) {(A1 A2)
(B1 B2)}
(9A.4b) Idem, in implicatie: Comprimatie, naar conjuncte premisse(n).
(9A.4c) Idem, in implicatie: Comprimatie, naar disjuncte conclusies.
9B. Connectief conversie: naar Disjunctie
.
Connectief-transformatie voor DNF conversie.
Omzetting van een formule naar een disjunctie van (conjuncties) van literalen.
Met name voor toetsing van premisse(n).
(Kan indirect bij CNF conversie bruikbaar zijn).
Alle geldig onder parafrase/ equivalentie.
9B.1
Connectief conversie: naar Disjunctie, algemeen.
Connectief-transformatie voor DNF conversie, via Syntactische vereenvoudiging.
(9B.1a) Conjunctie disjunctief omzetting.
(9A.1b) Negatief-implicatie disjunctief omzetting.
Bijv.: {¬(A B)} (¬(¬A
B)).
9B.2 Connectief conversie, naar Disjunctief
normaal vorm (DNF); divers.
Connectief-transformatie voor DNF conversie, divers.
(9B.2a) Implicatie normaal omzetting.
(9B.2b) Equivalentie disjunctief omzetting.
Bijv.: {A B} ((A
B) (¬A ¬B)).
(9B.2c) Exclusief disjunctie disjunctief omzetting.
Bijv.: {A # B} ((A ¬B)
(¬A B)).
9B.3 Connectief conversie, naar Disjunctie
; via Distributie.
Connectief-transformatie voor DNF conversie, via Distributie.
Extensie via verspreiden ( Distributie) van basale termen/ literalen.
Naar ( partiële) ' Symmetrische equivalentie' I, van geneste conjuncten.
(9B.3a) Distributie, naar disjunctie.
Verspreiden ( Distributie) van basale conjunct.
Met toenemende nesting complexiteit:
(9B.3a.1) Idem; Vanuit CNF, met atoom-diepte = 2.
Bijv.: {A (B C)};
(distr.) ((A B) (A
C)).
Bijv.: {(A1 A2) (B1 B2)}
(distr.1) (((A1 A2)
B1) ((A1 A2) B2) );
(distr.2) ((A1 B1)
(A1 B2) (A2 B1)
(A2 B2) ).
Bijv.: {(A B) (C D)};
[1e: hoofdconnectief (niveau 1) ' ' naar ' ':]
(distr.1) ((A B)
C)
((A B) D) );
[2e: genest connectief (niveau 2) ' ' naar ' ':]
(distr.2) (((A C)
(B C)) ((A D)
(B D)) );
((A C)
(A D) (B C)
(B D)).
Algemene structuur, in CNF:
{(A [1] .. A [n])
(B [1] .. B [m])};
(2xdistr.) {DNF: ((A [1] B
[1]) .. (A [1] B
[m])); .. ((A [n]
B [1]) .. (A [n] B [m]))}.
(9B.3b) Idem, in implicatie: Distributie, van conclusie(s).
(9B.3c) Idem, in implicatie: Distributie, van premisse(n).
9B.4 Connectief conversie: naar Disjunctie
, via Comprimatie.
Connectief-transformatie voor DNF conversie, via Comprimatie.
Reductie via samentrekken ( Contractie) van lokale termen/ literalen.
Wegens ( partiële) ' Symmetrische equivalentie' I, van geneste disjuncten.
Stap (1) Samentrekking (contractie) van conjuncte disjuncties,
op grond van minstens één gemeenschappelijke - parallel-equivalente - lokale disjunct.
Stap (2) Onttrekking (destillatie) van minstens twee parallel-equivalente lokale disjuncten, en transitie naar de hoofdlijn.
(9B.4a) Comprimatie, van lokale conjuncten naar basale disjunct.
Met toenemende nesting complexiteit:
(9B.4a.1) Idem; Vanuit CNF, met atoom-diepte = 2.
Bijv.: {(A1 B) (A1 C)}
(compr.)(u) (A1 (B
C) );
Bijv.: {(A1 B) (A1 A2)}
(compr.)(u) (A1 (A2
B) );
Niet verder reduceerbaar.
Tabelbewijs:.
(kolommen A1, A2, B):
Atc:
{(A1: $(1111.0000) B: $(1010.1010))
(A1: $(1111.0000) A2: $(1100.1100))};
( $(1111.1010) $(1111.1100));
$(1111.1000).
Csq:
{A1: $(1111.0000) (A2: $(1100.1100)
B: $(1010.1010))};
( $(1111.0000) $(1000.1000));
$(1111.1000) : geldig.
Bijv.: {(A1 B1) (A1
B2) (A2 B1) (A2
B2) }
(2xlok.compr.) ((A1 (B1
B2)) (A2 (B1 B2)) );
(bas.compr.) {(A1 A2)
(B1 B2)}
(9B.4b) Idem, in implicatie: Comprimatie, naar disjuncte premissen.
(9B.4c) Idem, in implicatie: Comprimatie, naar conjuncte conclusies.
9C. Syntactische reductie via Gecombineerde
vormen van Comprimatie en Distributie.
Transferente equivalentie tussen basale literaal en lokale literaal in geneste
literalengroep binnen complex element.
Reductie via Indirecte Comprimatie, via (directe) Distributie.
Géén Connectief conversie.
9C.1.
Combinatie van Comprimatie en Distributie; In Conjunctie.
Zie (10B.1a) Indirecte Complexe Transferente Disjunct Implicatie.
Reductie via (directe) Distributie, naar disjunctie; resp. Comprimatie, naar conjunctie.
9C.2. Combinatie van Comprimatie
en Distributie; In Disjunctie.
Zie (10B.2a) Indirecte Complexe Transferente Conjunct Implicatie.
Reductie via (directe) Distributie, naar conjunctie; resp. Comprimatie, naar disjunctie.
VII. Wetten voor Semantische Parafrase
Reductie.
Wetten voor reductie via eliminatie van redundante (deel)redenering ( clause) - alle onder parafrase/ equivalentie
.
O.a. bruikbaar t.b.v. Convergente reductie bewijsvoering (in PPL).
Reductie vanwege onderlinge implicatie van elementen binnen dezelfde hoofdformule.
(Waardoor één van die elementen geen informatieve waarde toevoegt).
Een element blijkt futiel, onwerkzaam, irrelevant; dus valt weg.
In CNF/ DNF.
Alle onder parafrase/ equivalentie.
10.
Parafrase reductie via Transferente equivalentie.
Tussen basale en geneste elementen.
Redundantie van meer complex element
Comprimatie, wegens 'Basale implicatie' Reductie:
(1) In CNF:
Via eliminatie van redundant 'zwakker' (gesubsumeerd, submessief) meer complex conjunct element (disjunctie
).
(2) In DNF:
Via eliminatie van redundant 'sterker' (subsumerend, dominant) meer complex disjunct element (conjunctie).
10A.
Directe Transferente equivalentie.
Transferente equivalentie tussen basaal element en lokaal (genest) element binnen complexe subformule.
O.a. Directe clause implicatie ( subsumptie); Disjunct Implicatie ( condensatie).
10A.1.
Directe Transferente equivalentie, in CNF (Conjunct Implicatie, Subsumptie
).
Transferente equivalentie tussen conjunct basaal element en lokaal element binnen (complexe)
conjuncte disjunctie(s).
De minder omvattende conjunct impliceert de complexe disjunctie: Clause implication.
Overtollige conjunctie(s).
Reductie via elimineren van basaal submissief (zwakker) conjunct element.
Reductie volgens principe: 'One-Literal Rule' (a) (Davis and Putnam, 1960).
Pragmatiek /Consequenties:
Fictieve/symbolische keuzeruimte.
'Luchtopties', 'Niet-bestendige contingenties' (overruled door 'harde feiten' op de baseline).
(10A.1a) Eenvoudige/ algemene vorm.
[Wet: {(p q) p } [
((p p ) (p q
) ); (u) (p (p
q ) );] [ (p (degres
) (p q ) );] (u)
p .]
Tabelbewijs:.
(kolommen p, q):
{((p: $(1100) q: $(1010))
( $(1110) ) p: $(1100)};
$(1100).
Bijv.: {A (A X)}
(u) A.
Bijv.: {A B (A C)}
(u) (A B).
Bijv.: {A1 (A1 A2 B)}
(u) A1.
Tabelbewijs:.
(kolommen A1, A2, B):
{A1: $(1111.0000) (A1: $(1111.0000)
A2: $(1100.1100) B: $(1010.1010))};
(A1: $(1111.0000) $
(1111.1110)); $(1111.0000).
(10A.1b) Meervoudige Transferente equivalentie.
Kiezen uit disjunctie en conjunctie.
Komt in CNF by default uit op conjunctie (sterkste claim van zekerheid). Via distributie
.
Bijv.: {(A B) (A B)}
(A B (A
B)); ((A B A)
(A B B) );
(2u) ((A B) (A
B) );
(2u) (A B).
(10A.1c) Complexe Transferente equivalentie.
Transferente equivalentie tussen basale literalengroep en literalengroep binnen complex
element.
Reducie via elimineren van complex element;
op grond van ' Complexe implicatie van subformule'.
Idem, in implicatie; in premisse(n).
Ook hier geldt het principe: de 'sterkere' conjunct overleeft in de confrontatie.
(1) Met disjuncte premisse(n).
(2) Met conjuncte premisse(n).
(10A.1d) Directe Transferente equivalentie, bij een (geneste) afleidingsregel.
Transferente equivalentie tussen conjuncte basale literaal en lokale conclusie binnen een
geneste afleidingsregel.
Pragmatiek /Consequenties:
Irrelevante redenering, die niet met enig effect toepasbaar is.
(1) Onecht Modus Ponens: Bewijs via evidente bevestiging.
Bijv.: {(A B) B}
((¬A B) B);
(u) B.
(2) Onecht Modus Tollens: Weerlegging via evidente negatie.
Bijv.: {(A B) ¬A}
((¬A B) ¬A);
(u) ¬A.
10A.2. Directe Transferente equivalentie
, in DNF (Disjunct Implicatie, Condensatie).
Transferente equivalentie tussen disjunct basaal element en lokaal element binnen (complexe)
disjuncte conjunctie(s).
De complexe conjunctie impliceert minder omvattende disjunct: Disjunct Implicatie.
Overtollige disjunct(en).
Reductie via elimineren van basaal dominant (sterker) disjunct element.
D.w.z. Condensatie (van disjunctie).
(10A.2a) Eenvoudige/ algemene vorm.
[Wet: {(p q ) p } [
((p p ) (p q ) );
(u) (p (p
q ) );] [ ((p q )
(degres) p );] (u) p. ]
Tabelbewijs:.
(kolommen p, q):
{((p: $(1100) q: $(1010))
$(1000) ) p: $(1100)};
$(1100).
Bijv.: {A (A X)}
(u) A.
Bijv.: {A B (A C)}
(u) (A B).
Bijv.: {A1 (A1 A2 B)}
(u) A1.
Tabelbewijs:.
(kolommen A1, A2, B):
{A1: $(1111.0000) (A1: $(1111.0000)
A2: $(1100.1100) B: $(1010.1010))};
(A1: $(1111.0000) $
(1000.0000)); $(1111.0000).
(10A.2b) Meervoudige Transferente equivalentie.
Kiezen uit disjunctie en conjunctie.
Komt in DNF by default uit op disjunctie (zwakste claim van zekerheid). Via distributie
.
Bijv.: {(A B) (A B)}
((A B) A
B); ((A B A)
(A B B) );
(2u) ((A B) (A
B) );
(2u) (A B).
Idem, indirecte vorm: Een redenering/afleidingsreeks vooronderstelt haar conclusie.
Drogreden: petitio principii.
Bijv.: {(A B) (B
A)}
(¬(¬A B) (¬B
A) ); ((A ¬B)
¬B A); (u)
(¬B A);]
(B A).
(10A.2c) Complexe Transferente equivalentie.
Transferente equivalentie tussen basale literalengroep en literalengroep binnen complex
element.
Reducie via elimineren van complex element;
op grond van ' Complexe implicatie van subformule'.
10B. Indirecte Transferente equivalentie
: Complexe Transferente implicatie.
Transferente equivalentie tussen basaal element en lokaal element in geneste literalengroep
binnen complex element.
Reductie via gecombineerde vormen van Comprimatie en Distributie:
(Directe) Distributie, resp. Indirecte Comprimatie.
10B.1.
Indirecte Transferente equivalentie, In Conjunctie.
(10B.1a) Indirecte Complexe Transferente Disjunct implicatie.
Reductie via (directe) Distributie, naar disjunctie; resp. Comprimatie, naar conjunctie.
Bijv.: {((A1 A2) B)
A2};
Route 1:
Basale Distributie (tot disjunctie).
(((A1 A2) A2)
(B A2) );
((A1 A2 A2)
(B A2) );
Eliminatie van lokale doublure.
(u) ((A1 A2)
(A2 B));
Basale Comprimatie (tot conjunctie).
Route 2:
Lokale Distributie (tot conjunctie).
(((A1 B) (A2
B)) A2);
((A1 B) (A2
B) A2);
Eliminatie wegens Basale Transferente equivalentie.
(Zie verder: 10A.1).
(u) (A2 (A1
B) ).
Niet verder reduceerbaar.
Tabelbewijs:.
(kolommen A1, A2, B):
{([A1: $(1111.0000) A2: $(1100.1100)]
B: $(1010.1010)) A2: $(1100.1100)};
(([ $(1100.0000)] B: $
(1010.1010)) A2: $(1100.1100));
(( $(1110.1010)) A2: $
(1100.1100));
$(1100.1000).
(10B.1b) Indirecte Transferente equivalentie, varianten met parallelle negatie.
{X \ (¬ X \ B)}
(¬X ¬(¬¬ X
¬B));
(¬X ¬( X
¬B));
(¬X (¬ X
B));
(u) ¬X.
10B.2. Indirecte Transferente equivalentie
, In Disjunctie.
(10B.2a) Indirecte Complexe Transferente Conjunct implicatie.
Reductie via (directe) Distributie, naar conjunctie; resp. Comprimatie, naar disjunctie.
Bijv.: {((A1 A2) B)
A2};
Route 1:
Basale Distributie (tot conjunctie).
(((A1 A2) A2)
(B A2) );
((A1 A2 A2)
(B A2) );
Eliminatie van lokale doublure.
(u) ((A1 A2)
(B A2) );
Comprimatie (tot conjunctie).
Route 2:
Lokale Distributie (tot disjunctie).
(((A1 B) (A2
B)) A2);
((A1 B) (A2
B) A2);
Eliminatie wegens Basale Transferente equivalentie.
(Zie verder: 10A.2).
(A2 (A1
B) ).
Niet verder reduceerbaar.
Tabelbewijs:.
(kolommen A1, A2, B):
{([A1: $(1111.0000) A2: $(1100.1100)]
B: $(1010.1010)) A2: $(1100.1100)};
(( $(1111.1100) B: $
(1010.1010)) A2: $(1100.1100));
(( $(1010.1000)) A2: $
(1100.1100));
$(1110.1100).
(10B.2b) Indirecte Transferente equivalentie, varianten met implicatie.
Contra-logische conclusie, in implicatie.
(1) Contra-logische conclusie, in implicatie, met disjuncte premissen.
Factief uitgesloten conclusie, met meervoudige ( disjuncte) premisse en onware referent premisse.
Contra-logica. Averechts, contra-logisch redeneren.
(2) Contra-logische conclusie, in implicatie, vanuit Modus Ponens.
Bijv.: (((A B) A )
¬B }
(¬((¬A B) A )
¬B );
((¬(¬A B) ¬A )
¬B );]
((A ¬B) ¬A
¬B );
(2u) (¬A ¬B );
(10B.2c) Indirecte Transferente equivalentie, varianten met exclusie.
{X | (¬ X | B)}
(¬X ¬(¬¬ X
¬B));
(¬X ¬( X
¬B));
(¬X (¬ X
B));
Basale Transferente equivalentie eliminatie (van disjuncte conjunctie).
(u) ¬X.
11. Parafrase reductie via Basale implicatie
.
11A.
Directe Basale implicatie.
11A.1.
Directe Basale implicatie; tussen Conjuncten.
Overtollige conjunct(en).
Directe Conjunct Implicatie.
Reductie door elimineren van (basaal) submessief, zwakker conjunct element.
D.w.z. Condensatie (van conjunctie).
(11A.1a) Directe 'Conjuncte waarheid' (verum).
Volgens ' Basaal-conjunct implicatie'.
Wet: [{(p (degres) $1 ) }
{(p $1 ) p }. ]
Tabelbewijs:.
(kolommen p, $1):
{p: $(1100) $(1111)}
$(1100). ]
(1) Idem, Directe 'Basale waarheid' (verum).
Bijv.: {A $1} [
(A (degres) $1);]
A.
(2) Idem, Directe 'Lokale waarheid' (verum).
Volgens ' Lokaal-conjunct implicatie'.
(11A.1b) Directe 'Conjuncte onwaarheid' (falsum).
Wet: [{( $0 (degres) p }
{(p $0 ) $0 }. ]
Tabelbewijs:.
(kolommen p, $0):
{p: $(1100) $(0000)}
$(0000). ]
(1) Idem, Directe 'Basale onwaarheid' (falsum).
Directe ' Fatale' contradictie; op grond van basale onwaarheid.
Volgens ' Basaal-conjunct implicatie'.
Bijv.: {A $0} [
($0 (degres) A);]
$0.
(2) Idem, Directe 'Lokale onwaarheid' (falsum).
Indirecte ' Niet-fatale' contradictie; op grond van lokale onwaarheid.
Volgens ' Lokaal-conjunct implicatie'.
11A.2. Directe Basale implicatie; tussen
Disjuncten.
Overtollige disjunct(en).
Directe Disjunct Implicatie.
Irrelevante optie(s), die niet toepasbaar zijn.
Reductie door elimineren van (basaal) dominant, sterker disjunct element.
D.w.z. Condensatie (van Conjunctie).
(11A.2a) Directe 'disjuncte waarheid' (verum).
[Wet: [{(p (degres) $1 ) }
{(p $1 ) $1 }.
]
Tabelbewijs:.
(kolommen p, $1):
{p: $(1100) $(1111) }
$(1111). ]
(1) Idem, Directe 'Basale waarheid' (verum).
Bijv.: {A $1} [
(A (degres) $1);]
$1.
(2) Idem, Directe 'Lokale waarheid' (verum).
(11A.2b) Directe 'disjuncte onwaarheid' (falsum).
(1) Idem, Directe 'Basale onwaarheid' (falsum).
Directe ' Niet-fatale' contradictie; op grond van lokale onwaarheid.
Volgens ' Basaal-disjunct implicatie'.
Bijv.: {A $0} [
($0 (degres) A);]
A.
Wet: [{( $0 (degres) p }
{(p $0 ) p }. ]
Tabelbewijs:.
(kolommen p, $0):
{p: $(1100) $(0000)}
$(1100). ]
(2) Idem, Directe 'Lokale onwaarheid' (falsum).
Indirecte ' Niet-fatale' contradictie; op grond van lokale onwaarheid.
Volgens ' Lokaal-disjunct implicatie'.
11B. Indirecte Basale implicatie.
11B.1.
Indirecte basale Implicatie; in Implicatie.
(11B.1a) Directe 'waarheid' (verum), in implicatie.
(1) Idem, Directe 'Basale waarheid' (verum), als premisse.
(2) Idem, Directe 'Basale waarheid' (verum), als conclusie.
Principe: 'Waarheid is altijd afleidbaar'.
Wet: ' Ex omnibus (dictum) vero reducantur'.
(11B.1b) Directe 'onwaarheid' (falsum), in implicatie.
(1) Idem, Directe 'Basale onwaarheid' (falsum), als premisse.
Principe: 'Uit onwaarheid is wat dan ook afleidbaar'.
Wet: ' Ex falso sequitur quodlibet'.
(2) Idem, Directe 'Basale onwaarheid' (falsum), als conclusie.
Indirecte ' Basale onwaarheid' (binnen disjunctie).
Inherent onmogelijke conclusie.
Concluderen tot onwaarheid, uit voorwaardelijke aanname.
(Directe) ' Niet-fatale' contradictie; in conclusie.
De bewering, redenering (betoog) of conclusie leidt tot onwaarheid - en blijkt daardoor onwaar.
Principe: Als iets tot een onwaarheid leidt, dan is het onwaar (dus ook onvervulbaar, dus ook ongeldig).
Het leidt dus tot ' Fatale reductie' (in PPL).
Volgens wetten van ' Reductio ad absurdum'.
(Zie ook: basiswetten t.b.v. bewijs door weerlegging van het tegendeel, ' elenctic refutation', Resolutie).
11B.2. Indirecte basale Implicatie
; tussen Disjuncten; in Equivalentie.
(11B.2a) Equivalentie aan directe 'Basale waarheid'.
(11B.2a.1) Een formule blijkt equivalent aan directe 'Basale waarheid' (verum).
Bijv.: {F $1 };
((F $1 )
( $1 F ) );
((¬F $1 )
(¬ $1 F ) );
((¬F $1 )
( $0 F ) );
Lokale gesubsumeerde disjunct eliminatie; Lokale disjuncte falsum eliminatie:
(( $1) (F) );
Basale conjuncte verum eliminatie:]
F [
F].
(11B.2a.2) Een redenering blijkt equivalent aan directe 'Basale waarheid' (verum).
Bijv.: {R $1 };
Afleiding verder analoog aan $(11B.2a.1).
R [
R].
(11B.2a.3) Een verzameling blijkt equivalent aan directe, 'Basale onwaarheid' (falsum).
Bijv.: {K * = { $1} };
((K *) $
$1 ); (K * $
1 );
Afleiding verder analoog aan $(11B.2a.1).
K * [
K*].
(11B.2b) Equivalentie aan directe 'Basale onwaarheid'.
(11B.2b.1) Een formule blijkt equivalent aan directe 'Basale onwaarheid' (falsum).
Bijv.: {F { $0 } };
[ CNF standaardisatie:
((F $0 )
( $0 F ) );
((¬F $0 )
(¬ $0 F ) );
((¬F $0 )
( $1 F ) );
Lokale disjuncte falsum eliminatie; Lokale gesubsumeerde disjunct eliminatie:
((¬F) $1) );
Basale conjuncte verum eliminatie:]
(¬F);
¬F [
¬F].
(11B.2b.2) Een redenering blijkt equivalent aan directe 'Basale onwaarheid' (falsum).
Bijv.: {R $0 };
Afleiding analoog aan $(11B.2b.1).
¬R [
¬R].
(11B.2b.3) Een verzameling blijkt equivalent aan directe, 'Basale onwaarheid' (falsum).
Bijv.: {K * = { $0} };
((K *) $
$0 ); (K * $
0 );
Afleiding verder analoog aan $(11B.2b.1).
¬K *; [
¬K*].
12. Parafrase reductie via 'Niet-fatale
' ('pseudo') contradictie.
Reductie via elimineren van ' globale/lokale redundantie', wegens ' Niet-fatale' contradictie;
vanwege implicatie, oftewel ' subsumptie' (onder unificatie).
In CNF/ DNF. Elimineren van 'zwakkere' elementen.
Alle onder parafrase/ equivalentie.
12A.
Directe 'Niet-fatale' ('pseudo') contradictie.
12A.1.
Directe 'Niet-fatale' ('pseudo') contradictie: tussen (lokale) Conjuncten
.
(12A.1a) Directe Lokale ('Niet-fatale
') contradictie; in DNF.
Reductie van redundantie in (lokale) disjunctie; wegens indirecte ' niet-fatale' (interne) logische strijdigheid.
Volgens ' (Lokale) implicatie', oftewel ' subsumptie' (onder unificatie).
Eliminatie van redundante literaal.
Via Factoriseren ( factoring) (in PPL).
Directe Lokale ('Niet-fatale') conjunct- contradictie; In DNF.
(12A.1b) Directe (lokale) 'Niet-fatale' ('pseudo') contradictie; via implicatie.
Concluderen tot contradictie, uit voorwaardelijke aanname.
Indirecte ' Basale onwaarheid' (binnen disjunctie); vanwege contradictie in conclusie, in een afleiding.
De bewering, redenering (betoog) of conclusie leidt tot complementaire beweringen, dus contradictie.
Reductie wegens ' Niet-fatale' contradictie.
(12A.1b.1) Concluderen tot contradictie; uit enkelvoudige voorwaardelijke aanname (literaal).
Als iets tot een contradictie (onvervulbaarheid) leidt, dan is het onwaar.
Negatie introductie regel.
(12A.1b.2) Idem; uit meervoudige voorwaardelijke aanname (conjunctie).
Bij de afleiding van een contradictie uit meerdere conjuncte aannamen volgt de weerlegging van minstens één
(deel)premisse.
Via Deductiestelling ( Deduction theorem).
Bijv.: {(A [1] ( .. (A [a]
(C ¬C ) ) .. ) );
((A [1], .. A [a] )
(C ¬C ) );
(¬(A [1], .. A [a] )
(C ¬C ) );
(u) (¬A [1] ..
¬A [a] $0 );
(¬A [1] .. ¬A [
a] ) }.
(12A.1b.3) Idem; uit complexe/ambivalente voorwaardelijke aanname (disjunctie).
Bij de afleiding van een contradictie uit meerdere disjuncte aannamen volgt de weerlegging van èlke (deel)premisse.
Bijv.: {((A [1] .. A [a] )
(C ¬C ) );
(¬(A [1] .. A [
a] ) (C ¬C ) );
((¬A [1] .. ¬A [
a] ) (C ¬C ) );
(u) ((¬A [1] ..
¬A [a] ) $0 );
(¬A [1] .. ¬A [
a] ) }.
(12A.1c) Directe (lokale) 'Niet-fatale' ('pseudo') contradictie; via Equivalentie.
Equivalentie aan directe ' Basale contradictie' ( unit conflict).
(12A.1c.1) Een formule blijkt equivalent aan directe 'Basale contradictie' (unit conflict).
( oxymoron).
Bijv.: {F (A ¬A) };
(u) (F $0 );
Afleiding verder analoog aan $(11B.2b.1).
¬F [
¬F].
(12A.1c.2) Een redenering blijkt equivalent aan directe 'Basale contradictie' (unit conflict).
Bijv.: {R (A [1] .. A [
i-1] A [i] ¬A [i
] A [i+1] ..
A [n] ) };
(u) (R (A [1] ..
A [i-1] $0
A [i+1] .. A [n] ) );
(R $0 );
Afleiding verder analoog aan $(11B.2b.2).
¬R [
¬R].
(12A.1c.3) Een verzameling blijkt equivalent aan directe, 'Basale contradictie' (unit conflict
).
Bijv.: {K * = {A [1] .. , A [i-1] , A [i]
, ¬A [i] , A [i+1] .. , A [n] } };
(u) (K * = (A [1] ..
A [i-1] $0
A [i+1] .. A [n] ) );
((K *) $ = $0 ); (K
* $0 );
Afleiding verder analoog aan $(11B.2b.3).
¬K * [
¬K*].
12A.2. Directe 'Niet-fatale
' ('pseudo') contradictie: tussen Disjuncten.
Directe ' Niet-fatale' disjunct- contradictie.
In de vorm van ' Tautologische (pseudo-)contingentie'.
(12A.2a) Directe Basale ('Niet-fatale') disjunct- contradictie; algemene vorm.
Complementaire disjunct-literalen. ' Tautologie' (in engere zin).
Tegenstrijdige opties, daardoor irrelevante opties, die niet toepasbaar zijn.
Tautologische Disjunctie-Reductie.
Reductie volgens principe: 'Tautology Rule' (Davis and Putnam, 1960).
Bijv.: {A ¬A} (u) $
1.
(12A.2b) Directe Lokale ('Niet-fatale') disjunct- contradictie; In CNF
.
M.n. (lokale) ' tautologie'. 'Tautologische (pseudo-)contingenties'.
' (Lokale) implicatie', oftewel ' subsumptie' (onder unificatie).
Reductie van redundante in (lokale) disjunctie.
Via Factoriseren ( factoring) (in PPL).
12B. Indirecte 'Niet-fatale
' ('pseudo') contradictie.
12B.1.
Indirecte 'Niet-fatale' ('pseudo') contradictie: tussen Disjuncten
.
Indirecte tautologie (in disjunctie).
(12B.1a) Indirecte Basale ('Niet-fatale
') disjunct- contradictie; via implicatie.
( Partiële) ' Symmetrische implicatie': I. onder parafrase; bij Transferente contradictie met
geneste implicatie.
(12B.1a.1) Een conclusie bevestigt de premisse, zodat de redenering altijd waar is.
(12B.1a.2) Uit het tegendeel van een eenmaal aangenomen bewering is elke conclusie afleidbaar.
(12B.1b) Indirecte Basale ('Niet-fatale') disjunct- contradictie; via exclusie (met
parallelle negatie).
Bijv.: { X | ( X \ A)}
(¬ X ¬( X | A));
(¬ X ¬(¬ X ¬A));
(¬ X ( X
A)); (¬ X X
A);
(u) ( $1 A);]
$1.
Bijv.: {(A \ X) | (A \ ¬ X)}
(¬(A \ X) ¬(A \ ¬ X) );
(¬(¬A ¬ X) ¬(¬A
¬¬ X) );
((A X)
(A ¬ X) ); (A
X A ¬ X );
(u) (A X
¬ X); (u) (A $
1 );
$1.
13. Parafrase reductie via Transferente
contradictie.
Reductie via elimineren van ' Lokale redundantie', wegens transferente contradictie van referent(en) op de
baseline, t.o.v. geneste elementen.
D.i. redundantie op grond van implicatie, oftewel ' subsumptie' (onder unificatie).
In CNF/ DNF.
[Wet: {(p ¬q) q }
((p q) (¬q q ) );
(u) ((p q)
( $0) ); (p q ) ].
Tabelbewijs:.
(kolommen p, q):
{((p:$(1100) ¬q: $(0101) )
q: $(1010) ) } ( $(1101)
q: $(1010) ); $(1000). ]
13A.
Directe Transferente contradictie.
Fictieve optie ( overruled door 'harde feiten' op de baseline).
Eliminatie van 'niet-duurzame optie'.
Transferente contradictie, connectief standaard vorm.
Betreft relatie tussen elementaire bewering ( unit clause) op de baseline en literaal binnen een subformule.
Redundantie van transferent-complementaire literaal.
Reductie volgens principe: ' One-Literal Rule' (b) (Davis and Putnam, 1960);
(I) Algemeen:
'Unit Resolution', 'U-resolutie'.
Reductie volgens principe: 'Unit resolution rule'.
Reduct: 'U-resolvent'.
(II) Speciaal geval: de resolvent is een unit clause.
D.w.z. de disjunctie wordt gereducteerd tot ('slaat neer' als) literaal op de hoofdlijn.
'Unit Resulting resolution', 'UR-resolutie'.
Reductie volgens principe: 'Unit resulting resolution rule'.
Reduct: 'UR-resolvent'.
(13A.1) Directe Transferente contradictie, in
CNF.
Betreft relatie tussen factieve bewering/ conjunct ( unit clause) op de hoofdlijn en disjunct element binnen een complexe
disjunctie, bijv. in afleidingsregel.
Redundantie van transferent-complementaire disjunct-literaal (in conjunctief normaal vorm, CNF
).
Bijv. vanuit aantoonbare feiten of geldige verbanden/wetten/regels.
(13A.1a) Eenvoudige/ algemene vorm.
(13A.1b) Directe Transferente contradictie, in CNF; de resterende disjunctie bevat enkel
positieve literalen.
Positive hyper-resolution.
Reductie volgens principe: 'Positive hyper-resolution rule'.
Bijv.: {(A B C)
¬B} (u) ((A C)
¬B).
(13A.1c) Directe Transferente contradictie, in CNF; de resterende disjunctie bevat enkel
negatieve literalen.
Negative hyper-resolution.
Reductie volgens principe: 'Negative hyper-resolution rule'.
Bijv.: {(¬A ¬B ¬C)
B} (u) ((¬A ¬C)
B).
(13A.2) Directe Transferente contradictie, in DNF.
Betreft relatie tussen voorwaardelijke bewering/ disjunct op de hoofdlijn en conjunct element binnen een complexe
disjunctie, bijv. in afleidingsregel.
Redundantie van transferent-complementaire conjunct-literaal (in disjunctief normaal vorm, DNF
).
Elimineren van complementaire conjunct;
op grond van ' Transferente contradictie'; in DNF.
(13A.2a) Eenvoudige/ algemene vorm.
13B.
Indirecte Transferente contradictie.
(13B.1) Indirecte Transferente contradictie; in
CNF.
(13B.1a) Indirecte Transferente contradictie, in CNF; bij een (geneste) afleidingsregel
.
Directe Transferente equivalentie tussen conjuncte basale literaal en lokale premisse
.
Indirecte vorm; via 'Conjunct-vervangingsregel'.
Bijv.
(13B.1a) Afleiding via 'bevestigende wijs': Modus Ponens
(MP).
Via Factief bevestigde premisse;
resp. (impliciete) Transferente contradictie eliminatie; resp. Conjunctieve reductie.
Eenvoudige vorm.
(Zie verder onder Modus Ponens).
(13B.1b) Weerlegging via 'ontkennende wijs': Modus Tollens (MT).
Via Factief uitgesloten conclusie;
resp. Contrapositie, c.q. Transpositie; resp. (impliciete) Transferente contradictie eliminatie reductie
; resp. Conjunctieve reductie.
Eenvoudige vorm.
(Zie verder onder Modus Tollens).
Directe Symmetrische equivalentie tussen conjuncte lokale literaal en lokale premisse
.
(13B.1b) Transferente equivalentie, in CNF; bij (geneste) equivalentie.
Indirecte Transferente equivalentie èn contradictie.
{A (A X)}
[ (A ((¬A X
) ((A ¬ X)));
(A (¬A X
) (A ¬ X));
Eliminatie wegens Transferente equivalentie (van basale disjunctie).
(u) (A (¬A
X));
Eliminatie wegens Transferente contradictie (van lokale disjunct ¬A).
(u) (A ( X));
(A X).
(13B.1c) Transferente contradictie, varianten met parallelle negatie.
Bijv.: {(B \ (A \ B)) \ (B \ (A \ B))}
[ CNF standaardisatie:
(¬(B \ (A \ B)) ¬(B \ (A \ B)) );
(¬(¬B ¬(A \ B) ) ¬(¬B
¬(A \ B) );
(¬(¬B ¬(¬A ¬
B) ) ¬(¬B ¬(¬A ¬B) ) );
((B (¬A ¬B) )
(B (¬A ¬B) ) );
Lokale Transferente contradictie eliminatie, 2x.
(2u) ((B ¬A)
(B ¬A) );
Basale doublure eliminatie.
(2u) (B ¬A);
(¬A B);]
(A B).
(13B.2) Indirecte Transferente contradictie; in DNF.
(13B.2a) Indirecte Transferente contradictie, in DNF; bij een (geneste) afleidingsregel
.
Directe Transferente equivalentie tussen disjuncte basale literaal en lokale conclusie
.
Irrelevante basale literaal, die niet met enig effect toepasbaar is.
Vormen van Indirecte basale (' Niet-fatale') contradictie tautologie.
Directe Symmetrische equivalentie tussen conjuncte lokale literaal en lokale premisse
.
(13B.2b) Directe Transferente equivalentie, in DNF; bij (geneste) equivalentie.
Bijv.: {A (A X)}
[ (A ((A X
) ((¬A ¬ X)));
(A (A X
) (¬A ¬ X));
Eliminatie wegens Transferente equivalentie (van basale conjunctie).
(u) (A (¬A
¬ X));
Eliminatie wegens Transferente contradictie (van lokale conjunct ¬A).
(u) (A ( X));
(A X).
(13B.2c) Directe Transferente contradictie, varianten met exclusie.
Bijv.: {X | ( X | B)}
[ CNF standaardisatie:
(¬X ¬(¬ X
¬B)); (¬X ( X
B));
Basale Transferente contradictie eliminatie.
(u) (¬X (B));]
(¬X B);
(¬X ¬(¬B));
(X | ¬B); (¬X ¬¬B);
(X B).
Bijv.: {X | ( X \ B)}
[ CNF standaardisatie:
(¬X ¬( X \ B));
(¬X ¬(¬ X
¬B));
(¬X ( X
B));
Basale Transferente contradictie eliminatie.
(¬X B).
(X B);]
(13B.3) Indirecte Transferente contradictie; in implicatie.
(13B.3a) Reductie bij identieke premisse(n).
{( A B1) ( A
B2)}
[ DNF standaardisatie:
(¬(¬ A B1)
(¬ A B2) ); (( A
¬B1) ¬ A
B2);
Lokale Transferente contradictie eliminatie.
(u) (¬B1 ¬ A
B2); ]
(( A B1)
B2). [(A
(B1 B2))].
(13B.3b) Reductie bij identieke conclusie(s).
{(A1 B) (A2
B)}
[ DNF standaardisatie:
(¬(¬A1 B)
(¬A2 B) ); ((A1
¬ B) ¬A2 B);
Lokale Transferente contradictie eliminatie.
(u) (A1 ¬A2
B);
(A2 (A1
B)). [((A1 A2)
B)].
14. Reductie via 'Symmetrische contradictie
', type I: onder parafrase.
Gecombineerd Symmetrische equivalentie èn contradictie;
al dan niet ' Gemengd', d.i. ' kruiselings verdeeld';
met daarnaast géén niet-unificeerbare elementen.
14A.
Reductie via (Partiële) 'Symmetrische contradictie': I. onder parafrase; eenvoudige vorm
.
Geldig onder parafrase/ equivalentie.
' Symmetrische contradictie', met daarnaast uitsluitend ' Symmetrische equivalentie'.
Gecombineerd Symmetrische equivalentie èn contradictie;
níet ' kruiselings verdeeld';
met daarnaast géén niet-unificeerbare elementen.
Reductie onder parafrase;
via Comprimatie met eliminatie van parallel-equivalente literalen,
resp. contractie met eliminatie van parallel-complementaire literalen.
Algemene structuur.
In CNF:
{( p q) (¬ p
q)};
Oftewel, nog algemener:
{( p q [1] ..
q [n]) ( ¬p
q [1] .. q [n])};
In DNF:
{( p q) (¬ p
q)};
Oftewel, nog algemener:
{( p q [1] ..
q [n]) ( ¬p
q [1] .. q [n])};
Bijv. {( A B) (¬ A
B)} [ {A,¬A} zijn unificeerbaar complementair, {B,B} zijn unificeerbaar equivalent]
Reductie geldig onder parafrase.
In CNF/ DNF: Contractie, via Comprimatie.
Wetten:
(1) Comprimatie op basis van unificeerbare c.q. gemeenschappelijke element(en).
[{( p q) ( p
r)} (u) ( p (q
r)).]
(2) Dus ook: [{( p q) ( p
¬q)} (u) ( p
(q ¬q)).]
(3) Verder: [{p ( q ¬ q
)} (u) (p ( $0)).]
(4) En: [{p ( $0)} p.]
(14A.1) In CNF: via Comprimatie
(naar disjunctie); waarna (lokale) Contradictie eliminatie.
(1) Basale Comprimatie (naar disjunctie).
(u) ((q [1] ..
q [n]) ( p
¬ p) );
(2) Lokale Contradictie eliminatie.
(u) ((q [1] ..
q [n]) $0 );
(3) Basale Onwaarheid implicatie eliminatie. Samenvoeging tot één basale disjunctie.
(q [1] ..
q [n] ).
Bijv.: {(A B) (A
¬B ) } (u) (A
(B ¬B)); (
u) (A ($0));]
A.
Bijv.: {( A B C)
( ¬A B C)}
(2u) ((A ¬A
) (B C));
(u) (($0) B C);
(B C).
Tabelbewijs:
(kolommen A, B, C):
[ ( $(1111.1110) $(1110.1111) );
(1110.1110); $
(1110.1110)].
Idem, varianten met (geneste) implicatie.
Idem, varianten met parallelle negatie.
Bijv.: {(A \ X) \ (A \ ¬ X)}
[ CNF standaardisatie:
[ {(A \ B) (¬A
¬B) ). ]
(¬(A \ X) ¬(A \ ¬ X) );
(¬(¬A ¬ X) ¬(¬A
¬¬ X) ); ((A X)
(A ¬ X) );
Comprimatie, naar disjunctie.
(u) (A ( X
¬ X) ); (u) (A ( $
0));]
A.
Reductie tot Exclusief-disjunctie.
Bijv.: {( A B) (¬
A ¬ B) }; (2u)
( A # B ).
(14A.2) In DNF: via Comprimatie (naar Conjunctie); waarna (lokale) Tautologie eliminatie
.
(1) Basale Comprimatie (naar conjunctie).
(u) ((q [1] ..
q [n]) ( p
¬ p) );
(2) Lokale Tautologie eliminatie.
(u) ((q [1] ..
q [n]) $1 );
(3) Basale Waarheid implicatie eliminatie. Samenvoeging tot één basale conjunctie.
(q [1] ..
q [n] ).
Idem, varianten met exclusie.
Bijv.: {(A | X) | (A | ¬ X)}
[ CNF standaardisatie:
[ {(A | B) (¬A
¬B) ); ]
(¬(A | X) ¬(A | ¬ X) );
(¬(¬A ¬ X) ¬(¬A
¬¬ X) ); ((A X)
(A ¬ X) );
Comprimatie, naar conjunctie.
(u) (A ( X
¬ X) ); (u) (A ( $
1));]
A.
Reductie tot Equivalentie.
Bijv.: {( A B) (¬
A ¬ B) }; (2u)
( A B ).
14B. Reductie via (Complete) 'Symmetrische
contradictie': I. onder parafrase; 'gemengde vorm'
.
Gecombineerd Symmetrische equivalentie èn contradictie;
' Gemengd', d.i. ' kruiselings verdeeld';
met daarnaast géén niet-unificeerbare elementen.
(14B.1) Reductie tot Equivalentie.
Equivalentie introductie regel.
Bijv.: {( A ¬ B) (¬
A B) }; (2u)
( A B).
(14B.2) Reductie tot Exclusief-disjunctie.
Bijv.: {( A ¬ B) (¬
A B) }; (2u)
( A # B ).
{Nb. Let op het verschil met deze vorm:
(Partiële) 'Symmetrische contradictie', met daarnaast ook niet-unificeerbare elementen.
Gecombineerd Symmetrische equivalentie èn contradictie; al dan niet 'kruiselings verdeeld', met daarnaast
óók niet-unificeerbare elementen.
Reductie alleen geldig onder degressie. Zie elders.}
C.P. van der Velde © 2004, 2015, 2018.
|
|