Alento Training Advies

**Methode 'Praktische Logica':**

Bewijsmethode voor Formele logica

**de Resolutiemethode.**

Inhoudsopgave

1. Inleiding

[

**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 S₀ van de te bewijzen stelling/ redenering R₀ .
(b) Stel het tegendeel van de te bewijzen stelling/ redenering R₀ (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 S₀*(_rst).
3. DD* : Contingentie-verzameling (disjuncties) van S₀*.
4. D* : Disjuncten-verzameling van S₀*.

**8. Subprocedure: Reductie tbv. Resolutie.**

Start lus/loop -1, per clausale formule S₀_(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 S₀_(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']


*Methode 'Praktische Logica':* Bewijsmethode voor Formele logica : *de Resolutiemethode.* Inhoudsopgave 1. Inleiding [ *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 S₀ van de te bewijzen stelling/ redenering R₀ . (b) Stel het tegendeel van de te bewijzen stelling/ redenering R₀ (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 S₀(_rst). 3. DD : Contingentie-verzameling (disjuncties) van S₀. 4. D : Disjuncten-verzameling van S₀. 8. Subprocedure: Reductie* tbv. Resolutie.** Start lus/loop -1, per clausale formule S₀_(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 S₀_(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']