(5.1) Equivalentie normaal omzetting
(5.2) Exclusief-disjunctie normaal omzetting
(5.3) Implicatie normaal omzetting
(5.4) Disjunctie normaal omzetting
(5.5) Disjunctie normaal
comprimatie
Via destillatie van conjuncten
(5.6) Conjunct-normaal
distributie
(verdeling)
Via spreiding van conjuncten over disjuncties
(5.6a) Vanuit DNF, met atoom-diepte = 2
(5.6b) Vanuit DNF, met atoom-diepte = 3
(5.6c) Vanuit DNF, met atoom-diepte = 4
(7.1) Reductie van (complexe)
proposities, wegens
redundantie
van
literalen; in CNV/DNV
Elimineren van atomaire
clause(s)
(negatieve of positieve atomaire proposities / predikaties).
(7.1a) Reductie van (complexe)
conjuncties; in CNV
Eliminatie van literalen op grond van '
Basale redundantie'.
Betreft relaties tussen
unit clauses
(literalen op de hoofdlijn).
(7.1a1) Elimineren van conjuncte literalen; op grond van 'Basale equivalentie'
(onder unificatie); in CNV.
(7.1a2) Elimineren van conjuncte literalen; op grond van 'Basale implicatie'
(onder unificatie); in CNV.
(7.1b) Reductie van (complexe)
disjuncties; in CNV/DNV.
Factoriseren
(
factoring) (in PPL):
Eliminatie van literalen op grond van '
Lokale redundantie'.
Betreft relaties tussen alternatieven/ disjuncten (literalen binnen disjuncties).
(7.1b1) Elimineren van disjuncte literalen; op grond van 'Lokale equivalentie'
(onder unificatie).
Eliminatie van doublure(s).
Principe: 'Propositional reduction rule', 'P-reduction'.
N(r) : operator van gereduceerde clauses verkregen door p-reductie.
Reduct: 'P-reduct'.
(7.1b2) Elimineren van disjuncte literalen; op grond van 'Lokale implicatie'
(onder unificatie).
Condensatie (van disjuncties).
Elimineren van 'lokaal-dominante' disjuncte elementen.
Volgens 'Lokaal-disjunct implicatieregel'
(7.1b2-sub) Op grond van 'Complexe implicatie van conjunctie' in CNV/DNV
DNV Conjunctie eliminatie regel.
(7.1c) Op grond van '
Complexe equivalentie'; in CNV
Betreft relatie tussen meerdere (complexe) disjuncties.
Zie (7.2a).
(7.2) Reductie wegens
redundantie
van (complexe)
disjuncties; in CNV
Elimineren van (complexe) disjuncties
Op grond van '
Globale redundantie', d.i. overtolligheid op de hoofdlijn.
(Alle onder
parafrase/
equivalentie).
(7.2a) Op grond van '
Complexe equivalentie'; in CNV
Betreft relatie tussen meerdere (complexe) disjuncties.
(7.2b) Op grond van '
Transferente equivalentie'; in CNV
Betreft relatie tussen een
unit clause
en een literaal binnen een complexe disjunctie.
De
unit clause
impliceert de complexe disjunctie.
Impliceert
Clause implication.
Disjunctief Syllogisme.
Principe: '
One-Literal Rule' (a) (Davis
Putnam, 1960):
(7.2c) Op grond van '
Complexe implicatie van disjunctie'; in CNV
Betreft relatie tussen (complexe) equivalenties.
De éne disjunctie is bevat in de andere.
CNV Conjunctie eliminatie regel.
(7.3) Reductie wegens '
Niet-fatale'
Contradictie; in CNV/DNV.
Elimineren van Redundanties, wegens
Contradictie
(Alle onder
parafrase/
equivalentie).
(7.3a) Reductie op grond van
Lokale onwaarheid; in CNV/DNV.
Speciaal geval van (7.1b2): '
Lokale implicatie' (onder unificatie).
Elimineren van 'zwakkere' elementen.
Volgens '
Lokaal-disjunct implicatieregel'.
(7.3b) Reductie wegens
basale contradictie
in
conclusie; in afleiding
De hoofdwetten tbv. '
Resolutie' c.q. '
Fatale reductie' (in PPL).
Tbv. Resolutie bewijsmethode.
Analoog aan (7.3a).
(7.3b1) Wegens onware conclusie uit ware bewering
(7.3b2) Wegens onware conclusie uit onware bewering
(7.3b3) Wegens strijdige conclusie uit (ware) bewering
(7.3c) Reductie op grond van '
Lokale contradictie'; in CNV/DNV
Betreft relaties binnen één disjunctie, m.n. (lokale) '
taulologie'.
'Tautologische (pseudo-)contingenties'.
Principe: '
Tautology Rule' (Davis
Putnam, 1960).
(7.3d) Reductie op grond van '
Transferente contradictie'; in CNF
Betreft relatie tussen een
unit clause
en een literaal binnen een complexe disjunctie.
Principe: '
One-Literal Rule' (b) (Davis and Putnam, 1960);
(a) Algemeen:
'Unit Resolution', 'U-resolutie'.
Principe: 'Unit resolution rule'.
Reduct: 'U-resolvent'.
(b) De resolvent is een
unit clause.
'Unit Resulting resolution', 'UR-resolutie'.
Principe: 'Unit resulting resolution rule'.
Reduct: 'UR-resolvent'.
(7.3d1) Met een tweeplaatsige disjunctie
(7.3d2) Met een méérplaatsige disjunctie
(7.3d3) De resterende disjunctie bevat enkel positieve literalen
Positive hyper-resolution
Principe: 'Positive hyper-resolution rule'.
(7.3d4) De resterende disjunctie bevat enkel negatieve literalen
Negative hyper-resolution
Principe: 'Negative hyper-resolution rule'.
(7.3e) Reductie op grond van '
Transferente contradictie'; in DNV
DNV conjunct eliminatie regel
(7.4) Reductie via Samentrekken (
Contractie) van (complexe) disjuncties; in CNV
Samentrekking (
contractie) van verschillende
clauses.
Met eventueel eliminatie van
equivalente literalen.
Op grond van '
Parallelle/ Symmetrische equivalentie' (onder unificatie).
D.i. (gedeeltelijke) equivalentie van complexe disjuncties.
(7.4a) '
Parallelle/ Symmetrische equivalentie', zonder tegelijk
'
Parallelle/ Symmetrische contradictie'; in CNV
Opties:
(7.4a1) Met toepassing van Conjunctie-splitsing
D.w.z. Complexe conjunctie reductie.
(Met degressie). (7.4a2) Contractie, daarna comprimatie wegens 'Lokale equivalentie
'
Met als gevolg 'Lokale redundantie' (zie ook elders).
Principe: 'Pure Literal Rule' (Davis and Putnam, 1960, p.43-52).
(Met degressie). (7.4a3) Met 'Parallelle/ Symmetrische implicatie' in CNF
(onder unificatie).
D.i. Disjunctief normaal Comprimatie
van conjuncte disjuncties.
(Onder parafrase/ equivalentie).
(Comprimatie, géén reductie!).
Zie ook (6.5) Conjunctie disjunctief comprimatie
(7.4b) '
Parallelle/ Symmetrische equivalentie', met tegelijk
'
Parallelle/ Symmetrische contradictie'; in CNV.
Zie hiervoor onder (7.5)
Reductie via Absorptie.
(7.5) Reductie via
Absorptie
Samentrekken (contractie) van disjuncties. Met eliminatie van
complementaire literalen.
Absorptie: De éne
clause (disjunctie) wordt opgenomen door een andere
clause (disjunctie).
Op grond van '
Parallelle/ Symmetrische contradictie'
D.i. contradictie tussen literalen van verschillende clauses
(onder unificatie).
Binaire resolutie;
'Propositional resolution', 'P-resolution'.
Principe: 'Resolution rule' (J.A. Robinson, 1965):
Operator: 'Propositional resolution rule', 'Binary resolution rule'.
Reduct: 'P-resolvent' (Géén equivalentie).
Varianten: (Sommige onder parafrase/ equivalentie, andere met degressie).
(7.5a) Met daarnaast uitsluitend
uniforme literalen, in PPL (c.q.
unificeerbare literalen, in PDL)
Reductie via Disjunctief normaal
Comprimatie
van conjuncte disjuncties;
Daarna eliminatie van lokale complementaire conjuncte literalen.
(Onder
parafrase/
equivalentie).
(7.5b) Met daarnaast uitsluitend
niet-unificeerbare literalen
Alleen symmetrische eliminatie van complementaire literalen
(Met
degressie).
(7.5c) Met
wel en niet-unificeerbare literalen
Opties: (Alle met
degressie).
(7.5c1) Alleen eliminatie van symmetrisch-complementaire literalen (vgl. 7.5b)
Eérst eliminatie van symmetrisch-complementaire disjuncte literalen.
Principe: 'Splitting Rule' (Davis and Putnam, 1960):
(7.5c2) Absorptie
Extra verlaging van logische kracht.
Eérst eliminatie van symmetrisch-complementaire disjuncte literalen;
daarna samentrekking (contractie) van disjuncties;
daarna eliminatie van lokaal-equivalente disjuncten.
(7.5c3) Absorptie, en vervolgens disjunctie-expansie
(7.5c4) Clause-eliminatie
Eérst samentrekking (contractie) van disjuncties;
daarna 'lokale contradictie', d.w.z. (lokale) taulologie;
daarna eliminatie van gehele disjunctie.
(7.5d) Wegens '
Dubbele Parallelle/ Symmetrische contradictie'
(onder unificatie).
Geen reductie van formule, maar vorm van comprimatie (met transformatie van hoofdconnectief).
Handig voor reductie van de verzameling literalen (Standaardisatie)
(Alle onder parafrase/ equivalentie).
(7.5d1) Reductie tot Equivalentie
(7.5d2) Reductie tot Exclusief-disjunctie
(8.1) Reductie op grond van '
Basale contradictie' (
unit conflict)
Betreft relatie tussen meerdere
unit clauses
op de hoofdlijn.
'Fatale' reductie: levert geslaagde
Resolutie.
T.b.v. bewijs door weerlegging van het tegendeel ('
Reductio ad absurdum').
(Alle onder
parafrase/
equivalentie).
(8.1a) Op grond van 'Complete contradictie'
Wegens Exclusief disjunctie.
(8.1b) Op grond van 'Basale falsificatie'
Wegens Implicatie
door basale onwaarheid.
(9.1) Substitutie via
Equivalentie
(9.1a) Transferente eliminatie van equivalentie
(9.1b) Equivalentie eliminatie regel ('≡ el')
(Is in feite een vorm van 'symmetrisch' modus ponens).
(9.2) Introductie of uitbreiding van
Implicatie
(9.2a) Implicatie introductie regel ('> in')
(9.2b) Voorwaardelijke negatieve premisse.
(9.2c) Implicatie toevoeging
(9.3) Wet van de
Contrapositie
(9.4) Substitutie via
Implicatie
Bewijs via 'bevestigende wijs'
Modus ponens (MP), '
Material detachment'.
Implicatie eliminatie regel ('> el')
(9.5) Weerlegging via 'ontkennende wijs'
Contrapositie,
Modus tollens (MT).
(9.5-sub) Weerlegging via evidente negatie
(9.6) Bewijs via 'ketenredenering', c.q. 'sluitredenering' (
syllogisme)
(versie PPL).
(9.6a) Regel van Algemeen syllogisme
(9.6b) Regel van keten redenering
[geen equivalentie!]
(9.7) '
Disjunct-implicatieregel'
(via transitiviteit). [geen equivalentie!]
(9.8) Disjunctie Eliminatie regel 'v el' ('officieel')
(9.9) Voorwaardelijke premisse-regel