Methode 'Praktische Logica':

   


Bewijsmethode voor Formele logica

:

de Resolutiemethode.



1. Inleiding tot Introductie Resolutielogica.


Een bijzonder krachtige bewijsmethode voor de formele logica, die behalve de propositielogica (PPL) ook de predikatenlogica (PDL) aankan, is die van resolutie.
{Zie o.m. John Alan Robinson (1965).}

Anders dan de bewijsmethoden van de PPL, zoals die van de waarheidswaardetabellen en de convergente reductie methode, werkt resolutie niet via positieve bewijsvoering maar volgens het principe van negatieve bewijsvoering.

Toetsing via logische falsificatie.


Het principe van 'negatieve' bewijsvoering is: als we de uitgangspunten van een redenering willen weerleggen, dan hoeven we alleen maar aan te tonen dat de eindconclusie van de redenering onwaar is. Want dan volgt logisch noodzakelijk dat het geheel van alle voorgaande argumenten, of redeneerschakels, althans in de hoofdlijn van de redenering, onwaar is - tot en met de eerste premisse.

Dit principe geldt ook voor een complex samenstel of netwerk van beweringen en redeneringen zoals een theorie of verklaringsmodel met betrekking tot een bepaald gebied in de werkelijkheid (zoals fysisch-empirisch domein of sociaal-empirisch domein).

De algemene redenering achter het principe van logische falsificatie-toetsing is deze. Een theorie of model vormt, samen met al zijn mogelijke implicaties en consequenties, in wezen één complexe ketenredenering met een bepaalde basislijn van premissen en conclusies. In die basislijn hoeven we echter maar één onware schakel te vinden. Zodra de logisch correct afgeleide consequenties van een model ergens uitlopen op een onwaarheid op de hoofdlijn van redenering - bijvoorbeeld vastlopen in een contradictie, hoe miniem ook - dan volgt daaruit dat het model zelf als geheel niet algemeen geldig is. Wanneer de gevonden contradictie steunt op een specifieke interpretatie, dan is bewezen dat het model niet in alle interpretaties consistent is - anders volgt dat het model als geheel zelfs inconsistent is.
Het maakt daarbij niet uit of het model hypothetisch, tentatief en voorlopig bedoeld is.

Met negatieve bewijsvoering kunnen we in principe twee kanten op:

(a)

Controleren van een model.


Meest voor de hand liggende toepassing van negatieve bewijsvoering is uiteraard toetsing van een model op logische vervulbaarheid via het checken van haar consistentie.

(a1)

Weerlegging van algemene geldigheid.


Deze aanpak is allereerst zeer effectief om bijvoorbeeld een bewering of betoog op een geldige manier te weerleggen, bijvoorbeeld van een opponent in een debat.

(a2)

Reparatie en optimalisering.


Het is daarnaast een uitstekende methode voor het controleren en toetsen van de eigen opvattingen en denkbeelden, om mogelijke tekortkomingen op te sporen, en deze waar mogelijk te repareren.
{N.b. Dit is bij uitstek nuttig wanneer het onderwerp of verwijzingsgebied behoort tot een 'open systeem', zoals de alledaagse werkelijkheid, fysisch, psychisch of sociaal. Typerend voor zulke domeinen is dat verschijnselen en categorieën niet eenduidig zijn af te bakenen, onbegrensd of 'onafzienbaar' zijn. Daardoor blijven onze gegevens over de werkelijkheid altijd enigszins 'fuzzy': onvolledig, onnauwkeurig en onzeker, blijven begrippen en termen die we ervoor gebruiken wat 'wollig', plooibaar en rekbaar, en blijven modellen en theorieën 'sloppy'. Toch kunnen we behoorlijke zekerheid krijgen over de betrouwbaarheid van kennis, wanneer we niet alleen zoeken naar bevestiging, maar vooral naar weerlegging van onze overtuigingen (het zgn. 'Falsificatie-principe'; vgl. Popper, K.R., 1934). Zie ook: Principes van 'Modelvorming'. De mogelijkheden van kennis, informatie en logica. }

Door falsificatie-toetsing verkrijgen we hoogwaardige informatie waarmee we onze kennis - relatief - kunnen verbeteren.
{N.b. Het is al sinds de oudheid in de filosofie bekend dat volmaakte kennis onbereikbaar is. Toch is het ontegenzeggelijk mogelijk om kennis te vergaren en te verbeteren. Zie ook: Bewijsvoering via falsificatie': In plaats van bevestiging, liever weerlegging zoeken.}

(a3)

Indirect bewijs van vervulbaarheid.


Verder kunnen we een model controleren op tekortkomingen om aan te tonen dat het tenminste niet tot contradicties leidt. Dit is een nuttige eerste stap als onderdeel van positieve bewijsvoering, waarbij we ook naar aanwijzingen en gegevens zoeken die de onderdelen van het model kunnen bevestigen (via verificatie).

(b)

Weerleggen van het tegendeel.


Een andere mogelijkheid die negatieve bewijsvoering biedt is het bewijzen van een model door aan te tonen dat het tegendeel onhoudbaar is.
De bedoeling is hierbij om het bewijs te leveren via negatieve bewijsvoering (falsificatie, refutatie): door weerlegging van het tegendeel of 'omgekeerde' van de te bewijzen stelling, middels afleiding van een contradictie (reductie ad absurdum).
Hiervoor is met name resolutie geschikt.


2. Uitgangspunten van Resolutie.



Resolutie is een methode van bewijsvoering door weerlegging van het tegendeel van wat te bewijzen staat.
Bij resolutie proberen we de logische geldigheid van een model te bewijzen door aan te tonen dat het omgekeerde van het model onhoudbaar is, want logisch onvervulbaar c.q. inconsistent. Dit door het aantonen van contradictie op de hoofdlijn van redenering (reductio ad absurdum).

Het (algemene) resolutie principe: is aantoonbaar correct en volledig.

Resolutie procedure :
Dient ten behoeve van bewijs van een theorema R0,
door middel van weerlegging van het tegendeel van R0, nl. S0.

De resolutie methode is bij uitstek geschikt in de fase van bewijsvoering, context of justification.

De resolutiemethode werkt in principe strikt syntactisch, het volgens formele regels combineren van symbolen.



Inhoud



Hieronder volgt een zeer beknopte inhoudsopgave van de overige onderdelen van deze cursusmodule.
De volledige weergave wordt aangeboden in de bijbehorende syllabus.
Voor bestellingen of meer informatie: Contact
.

Inhoud

(hoofdpunten):



3. Enkele basiswetten ten behoeve van Resolutie.



3.1.

In propositielogica (PPL).


Wetten voor 'reductio ad absurdum'
(•) Via 'Basale contradictie'.
(·) Wegens Exclusief disjunctie.
(·) Wegens 'Basale implicatie'.
(•) Via 'Lokale redundantie'.
(·) Wegens 'Lokale implicatie' (onder unificatie).

3.2

In predikatenlogica (PDL).


Reductie wegens conclusie met contradictie.
(a) Met contradictie over gehele domein.
(b) Met contradictie over gedeelte van domein.

3.3

In meta-logica.


(•)

Principe van bewijs door 'weerlegging van het tegendeel'


(Reductio ad absurdum):
(1) Uit geldigheid volgt vervulbaarheid, c.q. consistentie.
(2) Uit bewijsbaarheid van contradictie volgt inconsistentie, c.q. onvervulbaarheid, resp. ongeldigheid.
(3) Uit bewijsbaarheid van contradictie uit het tegendeel volgt geldigheid.
(•) Traject van weerlegging van het tegendeel.
(a) Semantisch.
(b) Syntactisch.

4. Globaal Schema voor Resolutie.



Strategie van resolutie.


Stappen.
1. Formuleer het tegendeel van R0.
2. Lever het bewijs dat S0 volledig onvervulbaar is (semantisch).
3. Lever het bewijs dat S0 inconsistent is (syntactisch).
Herleiding tot contradictie (reductio ad absurdum).
3a. Tijdelijke 'pseudo-aanname' van het 'contra-model'.
3b. Zet S0 om in conjunctief normaal vorm (CNV).
3c. Zet CNV(S0) om in verzameling conjuncten (clause set).
3d. Afleiding uit CNV(S0)* van een contradictie op de hoofdlijn van redenering.
4. Conclusie.

Voorbeeld van resolutie deductie.



5. Enkele vuistregels bij de resolutie procedure.



(1)

Vereenvoudiging


(1a) Conversie.
(1b) Universele afsluiting.
(1c) Kwantor eliminatie.
(1) Existentiële kwantor eliminatie.
(2) Universele kwantor eliminatie.
(1d) Reductie.
(1e) Reductio ad absurdum.

(2)

Vergroot de kans op unit conflict op de hoofdlijn.



(3)

Beperk de zoekruimte.


(3a) Maximaliseren van zekerheid.
(3b) Behoud van syntactische reikwijdte.
(3c) Behoud van referentiële reikwijdte.

(4)

Unificatie.



(5)

Most general unifier (mgu).



(6)

Afleiding van contradictie.



6. Resolutie-strategie: stappen in de procedure.



Begin procedure Resolutie.



Fase 1: Complementaire stelling.


(a) Construeer het tegendeel S0 van de te bewijzen stelling/ redenering R0.
(b) Stel het tegendeel van de te bewijzen stelling/ redenering R0 (pseudo-aanname).
(c) Conversie naar standaard formule vorm voor resolutie.
Formule-conversies t.b.v. Resolutie.

Fase 2. Omzetting naar Negatie normaal vorm (NNF).


Over-all negatie-binnenplaatsing.

Fase 3. (Predikatenlogica): Standaardiseren van kwantor-bindingen.


Subfase 3.a (Predikatenlogica): Onderscheid de variabelen naar hun bindende kwantor (QVNF).
Subfase 3.b (Predikatenlogica): Het identificeren van vrije variabelen (FVNF).
Subfase 3.c (Predikatenlogica): Het 'binden' van vrije variabelen (FVQ/ UQNF).

Fase 4. (Predikatenlogica) Omzetting in Prenex normaal vorm (PNF).



Fase 5. Omzetting in Logisch Normale Vorm (Conjunct normaal vorm, CNF).



Fase 6 (Predikatenlogica): Het elimineren van alle existentiële kwantoren.


Subfase 6.a (Predikatenlogica): Binding van variabelen aan conjuncten (CVNF).
Subfase 6.b (Predikatenlogica): Zet de formule om in Skolem Normaal Vorm (SkNV).
(6b.1) Eerst de variabelen van existentiële kwantoren die binnen bereik van n universele kwantoren staan:
(6b.2) Daarna de variabelen van existentiële kwantoren die buiten bereik van n universele kwantoren staan:

Fase 7 (Predikatenlogica): Eliminatie van alle universele kwantoren (QFNF).



Fase 8. Opsplitsen van de basisconjunctie in een verzameling conjuncten (disjuncties) (CFNF).



Fase 9. Resolveren (de eigenlijke Resolutieprocedure).


Recursief uitvoeren: stappen 9.1 en verder.
Stap 9.1. Sorteren voor reductie.
Stap 9.2. Opstellen van potentiële reductie-reeksen.
Stap 9.3. Opstellen van kandidaat-unificaties.
Stap 9.4. Voorbereiden van reductie, door unificatie (in PDL).
Stap 9.5. Uitvoeren van minstens één reductie-operatie.
Stap 9.6. Controleer op resultaten voor resolutie.
9.6a. Indien het 'reduct' bestaat uit de lege verzameling:
9.6b. Indien het 'reduct' geen lege verzameling oplevert:

Einde procedure Resolutie.





7. Hoofdgroepen in de clause set.


1. CL* : Verzameling Conjuncten, clauses.
2. C* : Hoofdlijn-verzameling van S0*(_rst).
3. DD* : Contingentie-verzameling (disjuncties) van S0*.
4. D* : Disjuncten-verzameling van S0*.

8. Subprocedure: Reductie tbv. Resolutie.



Start lus/loop -1, per clausale formule S0(i).
1. Subfase: Eliminatie van eventuele doublures en andere redundantie
1a. Syntactische 'bezuiniging' - op nesting-tekens (haakjes).
1b. Controleer strings van (resterende) conjuncten.
Start lus/loop -2a, per conjunct-literaal C(k1):
Zoek: Tautologie (verum) op de hoofdlijn, 'basale redundantie'.
Start lus/loop -3a, per C(k2), (waarbij: ¬(k1=k2)):
(a) Minstens twee conjuncten zijn onderling syntactisch identiek, of logisch equivalent;
Is 'basale equivalentie'; doublure(s), redundantie, (Redundancy).
(b) Idem, via instantiatie.
Sluit lus/loop -3a, per C(k2), (waarbij: ¬(k1=k2)).
Sluit lus/loop -2a, per C(k1).
2. Controleer het aantal (resterende) conjuncten.
3. Subfase. Eliminatie van eventuele contradicties.
3.1. Primaire Reductie - Categorie I.
Start lus/loop -2b, per C(k1):
Zoek: '$0' (falsum) op de hoofdlijn, 'basale falsificatie'.
3.1a. Zoek minstens één 'potentiële complementaire conjunct-literaal' C(k2).
Start lus/loop -3a, per C(k2), (waarbij: ¬(k1=k2)):
Zoek: twee complementaire conjuncten, 'basale contradictie' (unit conflict).
Idem, via instantiatie.
Zo ja: Stop. Resolutie geslaagd.
Sluit lus/loop -3a, per C(k2).
Sluit lus/loop -2b, per C(k1).
3.2. Secundaire Reductie - Categorie II.
Subdoel: het vergroten van resolutie-ruimte.
Start lus/loop -2c, per C(k1):
Start lus/loop -3b, per DD(h1).
Start lus/loop -4, per D(j1,l2,h1), (waarbij: ¬(l1=l2)), binnen de DD(h1):
3.2a. Tests voor eliminatie van de gehele disjunctie DD(h1).
(a) Binnen een disjunctie zijn twee disjuncten complementair.
Impliceert 'lokale contradictie'; m.n. (lokale) 'taulologie'.
(b) Een conjunct is identiek of equivelent aan een disjunct.
Impliceert 'transferente equivalentie'. Disjunctief Syllogisme.
Een conjunct impliceert een disjunct: 'transferente implicatie'.
3.2b. Tests voor 'uitdunning' (snoeien, trimming) van de disjunctie DD(h1).
(1) Een disjunct is '$0' (falsum).
Impliceert 'lokale redundantie'.
(2) Twee disjuncten zijn identiek of logisch equivalent: 'lokale equivalentie'.
(2a) Vormen onmiddellijk/ expliciet een equivalentie.
Evt. via permutatie; factorisatie.
Impliceert 'lokale equivalentie'.
(2b) Vormen niet onmiddellijk/ expliciet een equivalentie:
Impliceert 'lokale implicatie'.
3.2c. Controleer het aantal (resterende) disjuncten in de 'current' disjunctie DD(h1).
3.2d. Vergelijk de inhoud van de 'current' disjunctie DD(h1) met externe bronnen.
Start lus/loop -5, per D(j2,l3,h1), (waarbij: ¬(l2=l3), ¬(j1=j2)), binnen de DD(h1):
3.2d.1 Zoek een (tweede) 'transferent-complementaire conjunct-literaal'.
Start lus/loop -6a, per C(k3), (waarbij: ¬(k2=k3):
(a) Zoek: een conjunct is complementair met een disjunct: 'transferente contradictie'.
(b) Idem, via instantiatie.
Sluit lus/loop -6a, per C(k3).
3.2d.2 Inter-clauses reductie. Binaire resolutie.
Start lus/loop -6b, per DD(h2), (waarbij: ¬(h1=h2):
3.2d.2a. Zoek minstens één 'parallel/ symmetrisch identieke disjunct-predikatie'.
Start lus/loop -7, per D(j2,l4,h2) binnen de DD(h2).
3.2d.2a1. Zoek minstens één 'parallel/ symmetrisch-complementaire disjunct-literaal'.
3.2d.2a2. Zoek minstens één 'parallel/ symmetrisch-equivalente disjunct-literaal'.
Sluit lus/loop -7, per D(j2,l4,h2), binnen de DD(h2).
3.2d.2b. Zoek minstens één 'parallel/ symmetrisch-equivalente disjunctie' DD(h3) uit DD*.
Impliceert: 'Complexe' globale equivalentie - onder unificatie.
(sub1) Idem, via unificatie ('harmoniërende instantiatie'):
Twee disjuncties bevatten (enkel) disjuncten die onderling identiek of equivalent zijn, of elkaar over en weer impliceren.
Impliceert 'Complexe globale implicatie'.
(sub2) Idem, zonder mogelijkheid van instantiatie via directe substitutie:
o.a. Subsumptie.
[Einde stap (3.2d.2b)]
Sluit lus/loop -6b, per DD(h2).
[Einde stap (3.2d.1-2)]
Sluit lus/loop -5, per D(j2,l3,h1), binnen de DD(h1).
[Einde stap (3.2a-d)]
Sluit lus/loop -4, per D(j1,l2,h1), binnen de DD(h1).
Sluit lus/loop -3b, per DD(h1).
Sluit lus/loop -2c, per C(k1).
[Einde stap (3.1-2)]
[Einde Subfase (1-3)]
Sluit lus/loop -1, per S0(i).

Einde subprocedure Reductie tbv. Resolutie.



9. Unificatie algoritmen.



9.1. Het Unificatie-algoritme 'UNIFY'


Uitgangsgegevens (parameters)
ENTRY Procedure Unify1 (E1, E2; Sbs1, m )
ENTRY Function Unifier2 (E1, E2)
EXIT. [Function 'Unifier2']
EXIT. [Procedure 'Unify1']