Methode 'Praktische Logica':

 

Bewijsmethode voor Formele logica

:

de Resolutiemethode.



Inhoudsopgave




[

1. Inleiding tot Introductie Resolutielogica.

]



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



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']