Methode:Formele Logica©InleidingLogische bewijsvoeringBewijsmethoden in de logica[eerste website versie 15-05-2006]
[3de, herziene versie 11-10-2009] Inhoudsopgave1. Het bewijzen van stellingen en redeneringen: Theorem proving. 2. Bewijzen in positieve en negatieve richting. 2.1. Positief bewijs
: reconstructie van de complete afleiding.
3. Bewijsmethoden naar inhoud en structuur.
2.2. Negatief bewijs : uitsluiten van mogelijkheden die tegenstrijdigheid opleveren. 4. Bewijsmethoden met toenemende reikwijdte. 1. Het bewijzen van stellingen en redeneringen: Theorem proving.
Er zijn twee globale strategieën voor logische bewijsvoering. 2.1. Positief bewijs: reconstructie van de complete afleiding.Een voor de hand liggende methode van bewijzen is zoeken naar positieve aanwijzingen en voorwaarden voor de waarheid van de te bewijzen stelling, deze 'bouwstenen' vervolgens te ordenen in een redeneerketen, en te toetsen of die als een 'bewijsreeks' kan dienen die de beoogde conclusie via logische afleiding oplevert. Hoe kan zo'n bewijsreeks in elkaar steken? Als eerste kunnen we voorlopig aannemen dat zo'n
bewijsreeks voor de te bewijzen stelling in een bepaald systeem
S!voor redenering en waarheidsvinding al bestaat, d.w.z. in een selectie van daar aanwezige elementen en hun onderlinge relaties, en dus alleen maar hoeft te worden 'ontdekt'. Als we uitgaan van de opbouw en samenstelling van de te bewijzen stelling kunnen we kijken of we het gevolgde redeneerpad inS!kunnen reconstrueren. We beginnen met het terugzoeken van bruikbare onderdelen (zgn. backtracking). De passende onderdelen selecteren we op hun logische kracht (relatieve bewijskracht) als 'schakels' in het bewijs.Deze bewijsmethode wordt ook constructivistisch genoemd, de bedoeling is om het bewijs op te bouwen via positieve bewijsvoering of bevestiging (verificatie, affirmatie): op grond van logische afleiding ( derivatie). De bewijsreeks heeft dan de vorm van een complete stap-voor-stap afleidingsreeks, die vanaf uitgangspunten (axioma's) van S!een expliciet pad volgt naar de eindconclusie. De vereiste bewijs reeks is dan ook extensioneel.Uiteraard kan de 'bewijsroute' daarbij allerlei omwegen volgen, dus overtolligheid bevatten. Maar het mooiste is als ze de kortste route volgt, dus rechtstreeks op haar doel afgaat. Het zoekproces is hier dus top-down, de bewijsconstructie is bottom-up. {Nb. Bijvoorbeeld het systeem van natuurlijke deductie, volgens Gerhard Gentzen (1934),
Frederic B. Fitch (1952).}
Analyse in disjunctief normaal vorm (
|
Bij positieve bewijsvoering is het doel om tenminste één voldoende voorwaarde te vinden voor de waarheid c.q. geldigheid van de verzameling van te bewijzen beweringen of redeneringen, c.q. de theorie. We zoeken dus disjunctieve deelverzamelingen die als alternatieve premissen kunnen dienen voor een bepaalde theorie. Voor dat doel is het handig om de gehele verzameling eerst om te zetten in een disjunctie van conjuncties, oftewel een disjunctief normaal vorm (
DNF
).2.2. Negatief bewijs: uitsluiten van mogelijkheden die tegenstrijdigheid opleveren.
Een 'secundaire' methode van bewijzen bestaat uit het systematisch testen en uitsluiten van alternatieve mogelijkheden voor de eindconclusie (via reductie), net zolang totdat de beoogde conclusie als enige logische mogelijkheid overblijft.
Hierbij beginnen we met het uitwerken van de beschikbare gegevens naar hun logische implicaties,
via 'voorwaarts redeneren' (zgn. forward chaining). We selecteren de consequenties op hun bewijskracht
voor de gewenste reductie.
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).
Het is bij deze methode dus voldoende om twee tegengestelde beweringen af te leiden op de hoofdlijn van redenering. Deze hoeven niet per se geïnterpreteerd te zijn in termen van basiselementen van het systeem (axioma's of bewezen stellingen). Daarom kan de bewijsreeks zeer abstract blijven, zodat de opbouw ervan niet per se afhankelijk is van een nadere interpretatie of 'concretisering' van variabelenamen met behulp van een bepaald domein. Dit betekent dat de bewijsreeks intensioneel kan blijven.
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).
{Nb. Een 'negatief bewijs' van een stelling A is dus net als 'positief bewijs' nog steeds
protagonistisch van aard ten aanzien van A: het heeft als strekking A te bewijzen (als waar of geldig).
Negatief bewijs volgt daarbij enkel een andere route - het maakt gebruik van de wet van dubbele negatie.
Dit niet te verwarren met weerlegging van A, dat uiteraard antagonistisch is ten aanzien van A,
dus precies de tegenovergestelde strekking heeft: nl. A te weerleggen.
De strekking is overigens taalkundig-logisch afleidbaar, en zegt niet per se iets over de achterliggende intentie (psychische toestand) noch over het behaalde resultaat (slagen van bewijsvering of weerlegging). }
De strekking is overigens taalkundig-logisch afleidbaar, en zegt niet per se iets over de achterliggende intentie (psychische toestand) noch over het behaalde resultaat (slagen van bewijsvering of weerlegging). }
Het is bij deze methode dus voldoende om twee tegengestelde beweringen af te leiden op de hoofdlijn van redenering. Deze hoeven niet per se geïnterpreteerd te zijn in termen van basiselementen van het systeem (axioma's of bewezen stellingen). Daarom kan de bewijsreeks zeer abstract blijven, zodat de opbouw ervan niet per se afhankelijk is van een nadere interpretatie of 'concretisering' van variabelenamen met behulp van een bepaald domein. Dit betekent dat de bewijsreeks intensioneel kan blijven.
{Een voorbeeld van zo'n intensioneel bewijs is het bewijs voor de Compactheid
van de eerste-orde predikatenlogica. Zie voor een samenvatting in:
Beperkingen van formele systemen. De grenzen die de logica aan zichzelf stelt..}
Het zoekproces en de bewijsconstructie verlopen hierbij top-down.
{Nb. Bijvoorbeeld de methode van resolutie, volgens John Alan Robinson (1965) e.a..}
Analyse in conjunctief normaal vorm (CNF
).
Bij 'negatieve' bewijsvoering is het doel om tenminste één voldoende voorwaarde te vinden voor de onwaarheid c.q. ongeldigheid van een verzameling van te weerleggen beweringen of redeneringen (die zoals gezegd het tegendeel c.q. complement vormt van de verzameling van te bewijzen beweringen, c.q. de theorie). We zoeken daarom in deze verzameling minstens twee deelverzamelingen die in conjunctie een contradictie vormen, waardoor de gehele complementaire verzameling weerlegd wordt. Voor dat doel is het handig om de gehele complementaire verzameling eerst om te zetten in een conjunctie van disjuncties, oftewel een conjunctief normaal vorm (
CNF
).3. Bewijsmethoden naar inhoud en structuur
3.1. Semantisch bewijs.
Bewijs van algemene logische geldigheid van een relatie tussen elementen.
Bijv. volgens de waarheidswaardentabellenmethode (positief bewijs), de boommethode (negatief bewijs), enz..
Bijv. volgens de waarheidswaardentabellenmethode (positief bewijs), de boommethode (negatief bewijs), enz..
3.2. Syntactisch bewijs.
Bewijs van logische afleidbaarheid van een ordeningspatroon.
Bijv. volgens de methode van natuurlijke deductie (positief bewijs), de resolutiemethode (negatief bewijs), enz..
Bijv. volgens de methode van natuurlijke deductie (positief bewijs), de resolutiemethode (negatief bewijs), enz..
4. Bewijsmethoden met toenemende reikwijdte
4.1. Bewijsmethoden - voor de propositielogica (PPL
).
(4.1a)
Oftewel de methode Schröder-Peirce.
We beschouwen elke elementaire bewering of propositie als logische variabele, en gaan uit van het bereik van mogelijke waarden voor die variabele (het meest efficiënt is binair, bijvoorbeeld {waar, onwaar}, {ja, nee}, {aan, uit}, {intern, extern}, (0, 1}, enz.). We hanteren een aantal regels voor de waarden die samengestelde propositie s, op basis van logische voegwoorden (operatoren, connectieven), met die combinaties van proposities aannemen. Dan bekijken we de verzameling van alle propositienamen in de formule, en deze ordenen we lexicografisch (naar lengte resp. alfabet). We maken een tabel met in de kolommen eerst de enkelvoudige (atomaire) propositienamen en als rijen alle mogelijke combinaties van waarheidswaarden die de proposities kunnen hebben. In de rechterkolommen vullen we de samengestelde (complexe) proposities in, tot en met de gehele formule. Uiteindelijk blijkt in deze laatste kolom op wat voor waarheidswaardepatroon de formule uitkomt: geldig, contingent of onvervulbaar.
Conjunctief normaal vorm van Implicatie.
{(A
B)} ≡ (¬A 
B).
(9.4c) Regel van Algemeen modus ponens.
Substitutie via Implicatie.
(9.4c.1) Bewijs via 'bevestigende wijs'.
Sluitrede, Modus ponens (MP), 'Material detachment'.
{(A B), A} B.
(4.1b)
Oftewel Convergente reductiemethode.
Dit is een variant van de axiomatische methode. Hierbij vindt herleiding plaats van een formule tot haar waarheidswaarde, of als dit niet lukt tot de meest eenvoudige, equivalente, niet verder reduceerbare variant ervan. Dit door omzetting via parafrasetransformatie naar een conjunctie van disjuncties (conjunctief normaal vorm, CNV), en vervolgens vereenvoudiging daarvan (parafrasereductie). De bedoeling is dat de CNV formule wordt teruggebracht (gereduceerd) tot de meest eenvoudige vorm die direct afleidbaar is uit de premisse (n): met volledig behoud van logische kracht, oftewel parafrase van de conclusie.
In
Methode van Waarheidswaardentabellen.
Oftewel de methode Schröder-Peirce.
We beschouwen elke elementaire bewering of propositie als logische variabele, en gaan uit van het bereik van mogelijke waarden voor die variabele (het meest efficiënt is binair, bijvoorbeeld {waar, onwaar}, {ja, nee}, {aan, uit}, {intern, extern}, (0, 1}, enz.). We hanteren een aantal regels voor de waarden die samengestelde propositie s, op basis van logische voegwoorden (operatoren, connectieven), met die combinaties van proposities aannemen. Dan bekijken we de verzameling van alle propositienamen in de formule, en deze ordenen we lexicografisch (naar lengte resp. alfabet). We maken een tabel met in de kolommen eerst de enkelvoudige (atomaire) propositienamen en als rijen alle mogelijke combinaties van waarheidswaarden die de proposities kunnen hebben. In de rechterkolommen vullen we de samengestelde (complexe) proposities in, tot en met de gehele formule. Uiteindelijk blijkt in deze laatste kolom op wat voor waarheidswaardepatroon de formule uitkomt: geldig, contingent of onvervulbaar.
{Naar: Benjamin Peirce (1809-1880), Friedrich Wilheml Karl Ernst Schröder (1841-1902), e.a..}
Voorbeelden.
Conjunctief normaal vorm van Implicatie.
{(A
B)} ≡ (¬A B).| (1) | (2) | (3) | (4) | (5) | (6) |
| A | B | ¬(1) | (3 2) |
(1 2) |
(4  5) |
| 1 | 1 | 0 | 1 | 1 | 1 |
| 1 | 0 | 0 | 0 | 0 | 1 |
| 0 | 1 | 1 | 1 | 1 | 1 |
| 0 | 0 | 1 | 1 | 1 | 1 |
Substitutie via Implicatie.
(9.4c.1) Bewijs via 'bevestigende wijs'.
Sluitrede, Modus ponens (MP), 'Material detachment'.
{(A
B), A} B.| (1) | (2) | (3) | (4) | (5) | (6) | (7) |
| A | B | (1 2) |
(1  3) |
(1 2) |
(4 5) |
(6 2) |
| 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| 1 | 0 | 0 | 0 | 0 | 0 | 1 |
| 0 | 1 | 1 | 0 | 0 | 0 | 1 |
| 0 | 0 | 1 | 0 | 0 | 0 | 1 |
(4.1b)
Methode van Parafrasereductie naar waarheidswaarde.
Oftewel Convergente reductiemethode.
Dit is een variant van de axiomatische methode. Hierbij vindt herleiding plaats van een formule tot haar waarheidswaarde, of als dit niet lukt tot de meest eenvoudige, equivalente, niet verder reduceerbare variant ervan. Dit door omzetting via parafrasetransformatie naar een conjunctie van disjuncties (conjunctief normaal vorm, CNV), en vervolgens vereenvoudiging daarvan (parafrasereductie). De bedoeling is dat de CNV formule wordt teruggebracht (gereduceerd) tot de meest eenvoudige vorm die direct afleidbaar is uit de premisse (n): met volledig behoud van logische kracht, oftewel parafrase van de conclusie.
In
PDL
-I zijn vaak 'ad hoc' interpretaties nodig van variabelen (d.i. instantiaties) om kwantoren weg te werken - via Skolem normalisatie - en om de laatste stap van de premisse(n) naar de conclusie te kunnen maken.Voorbeelden.
(9.4) {(A B) A}
B.
Modus ponens.
Implicatie Eliminatie regel, '> el'.
B) A}
B.Modus ponens.
Implicatie Eliminatie regel, '> el'.
(a)
≡ ((¬(A B) A)
B);
≡ (¬((¬A B) A)
B);
[Wet: ¬(X Y) ≡ (¬X
¬Y) ]
≡ ((¬(¬A B) ¬A)
B);
[Wet: ¬(¬X Y) ≡ (X
¬Y) ]
≡ (((A ¬B) ¬A)
B);
≡ (((A ¬B) ¬A
B) (
Distributie:
≡ ((A ¬A B)
(¬B ¬A B)) (
≡ (((A ¬A) B)
(¬B ( B) ¬A));
Reductie:
≡ ((( B) (( ¬A));
≡ (( (
≡
(b)
CNV
van gehele formule:≡ ((¬(A
B) A)
B);≡ (¬((¬A
B) A)
B);[Wet: ¬(X
Y) ≡ (¬X
¬Y) ]≡ ((¬(¬A
B) ¬A)
B);[Wet: ¬(¬X
Y) ≡ (X
¬Y) ]≡ (((A
¬B) ¬A)
B);≡ (((A
¬B) ¬A
B) (DNV
);Distributie:
≡ ((A
¬A B)
(¬B ¬A B)) (
CNV
);≡ (((A
¬A) B)
(¬B ( B) ¬A));Reductie:
≡ (((
$
1) B) (($
1) ¬A));≡ ((
$
1) ($
1));≡
$
1 (d.i. geldig).(b)
CNV
van premisse resp. conclusie:(b1)
≡ ((¬A B) A);
Distributie:
≡ ((¬A A) (B
A));
≡ ( (B A));
Reductie:
≡ (A B);
Conjunct destillatie:
B
(b2)
≡ B;
(3) ((1) (2));
(4) ≡
CNV
van premisse:≡ ((¬A
B) A);Distributie:
≡ ((¬A
A) (B
A));≡ (
$
0 (B A));Reductie:
≡ (A
B);Conjunct destillatie:
B (b2)
CNV
van conclusie:≡ B;
(3) ((1)
(2));(4) ≡
$
1 (d.i. geldig).4.2. Bewijsmethoden - voor de predikatenlogica, van de eerste orde (PDL
-I).
(D.w.z. ook voor
PPL
)(4.2a)
Herleiding, of axiomatische methode.
Herleiding van een aantal formules tot een bepaalde conclusie, via een aaneenschakeling van tussenstappen. Dit met behulp van een beperkte verzameling van hulpstellingen in de vorm van logische wetten (axioma 's, d.i. bewezen theorema's). De verbindingen tussen 'schakels' en hulpstellingen berusten typisch op substitutie wetten (m.n. modus ponens).
[D3] (MP)
(4.2b)
Oftewel Natural deduction. Doelgerichte afleiding van een formule uit een gegeven verzameling formules. (naar G. Gentzen, 1934; F.B. Fitch, 1952).
De structuur van het bewijs bestaat uit een hoofdlijn van redenering, waarop elementaire conjuncten (unit clauses ) en eventuele disjuncties worden geplaatst, de laatste in de vorm van geneste redeneerlijnen (subderivaties).
Afleiding vindt plaats met behulp van een beperkte, vaste verzameling van afleidingsregels (per connectief één regel voor introductie en één regel voor eliminatie).
Implicatie eliminatie regel, '> el' (volgens modus ponens).
(4.2c)
Een klassieke variant van de reductiemethode is 'Herbrand logica' (J. Herbrand, 1931). Hierbij wordt uitsluitend van domeininterpretaties gebruik gemaakt waarbij alle variabelen worden vervangen door object constanten, zgn. ' grondsubstituties'.
Zie hieronder, (4.2d) 'Methode van Minimaal domein definitie'.
(4.2d)
Een praktische combinatie van Convergente reductiemethode en Herbrand interpretatie, die geschikt is voor predikatenlogica, vind je in de Minimaal domein definitie bewijsmethode.
Modus ponens (MP), in
D.w.z. met factieve premisse (referent) existentieel.
(4.2e)
Oftewel Tableaumethode, boomdiagram-methode.
Toetsing van de geldigheid van een redenering door weerlegging van de onvervulbaarheid van het tegendeel.
Met name wordt onderzocht of er contradictie schuilt tussen de premisse(n) en het tegendeel van de conclusie. Voor dit doel worden de premisse(n) en de negatie van de conclusie tezamen in een conjunctief normaal vorm gebracht, waarna de disjuncties worden uitgesplitst in hun disjuncten, een 'tak' per disjunct. De bedoeling is om in de complementaire conclusie minstens één conjunct te vinden waarvan elke disjuncte 'tak' strijdig is met elke disjuncte 'tak' van minstens één conjunct in de premisse(n). In dat geval blijkt contradictie tussen conjuncten van complementaire conclusie en van premisse(n). Daarmee is onvervulbaarheid van het tegendeel aangetoond, dus geldigheid van de te toetsen bewering.
(4.2f)
Deze methode is gebaseerd op het principe van toetsing van de te bewijzen redenering via weerlegging van het tegendeel, door het afleiden van een uitzondering of tegenvoorbeeld van het tegendeel. (reductio ad absurdum). Ook hier worden de premisse(n) en de negatie van de conclusie tezamen in een conjunctief normaal vorm gebracht. Hieruit wordt vervolgens een verzameling van kwantor-vrije, Skolem-normaal conjuncten afgeleid (de clause set). Doel is afleiding van minstens één lege verzameling conjuncten op de hoofdlijn van redenering, uit complementair e conjuncten in conclusie en in premisse(n). Van elk van die conjuncten is minstens één consequentie, afgeleide of interpretatie nodig. Hierbij kan gebruik worden gemaakt van regels voor reductie, resolutie en (in
Bewijs via resolutie (in
Methode van Axiomatische bewijsvoering.
Herleiding, of axiomatische methode.
Herleiding van een aantal formules tot een bepaalde conclusie, via een aaneenschakeling van tussenstappen. Dit met behulp van een beperkte verzameling van hulpstellingen in de vorm van logische wetten (axioma 's, d.i. bewezen theorema's). De verbindingen tussen 'schakels' en hulpstellingen berusten typisch op substitutie wetten (m.n. modus ponens).
{Zie o.a.: Bertrand Russell (1903): 'Principles of mathematics', London: Norton, 1903.
Bertrand Russel & Alfred North Whitehead (1910, 1912, 1913): 'Principia Mathematica', 3 volumes, 1910 (Vol. 1), 1912 (Vol. 2), 1913 (Vol. 3). England, Cambridge: Cambridge University Press. Second edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Cambridge: Cambridge University Press.}
Bertrand Russel & Alfred North Whitehead (1910, 1912, 1913): 'Principia Mathematica', 3 volumes, 1910 (Vol. 1), 1912 (Vol. 2), 1913 (Vol. 3). England, Cambridge: Cambridge University Press. Second edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Cambridge: Cambridge University Press.}
Voorbeelden.
[D3] (MP)
Modus ponens.
{ (K* 
F )
(Ks* 
K
* )
( (Ks* (F
G ) );
( (Ks* G
) (F G ) );
( (Ks* G
) ) (K* G ) );
((K* 
Ks*
) G ) ) ) ) }.
{ ( (F G )
F )
G }.
F )(Ks* K
* ) ( (Ks* (F
G ) ); ( (Ks* G
) (F G ) ); ( (Ks* G
) ) (K* G ) );((K* Ks*
) G ) ) ) ) }.{ ( (F G )F )G }.(4.2b)
Methode van Natuurlijke deductie
Oftewel Natural deduction. Doelgerichte afleiding van een formule uit een gegeven verzameling formules. (naar G. Gentzen, 1934; F.B. Fitch, 1952).
De structuur van het bewijs bestaat uit een hoofdlijn van redenering, waarop elementaire conjuncten (unit clauses ) en eventuele disjuncties worden geplaatst, de laatste in de vorm van geneste redeneerlijnen (subderivaties).
Afleiding vindt plaats met behulp van een beperkte, vaste verzameling van afleidingsregels (per connectief één regel voor introductie en één regel voor eliminatie).
{Zie o.a.: G. Gentzen (1934): 'Untersüchungen uber das logische Schließßen',
Mathematische Zeitschrift 39: pp.176-210, 405-431. In the French translation:
'Récherches sur la déduction logique, 1955.
F.B. Fitch (1952): 'Symbolic Logic. An Introduction'. New York, Ronald Press.}
F.B. Fitch (1952): 'Symbolic Logic. An Introduction'. New York, Ronald Press.}
Voorbeelden.
Implicatie eliminatie regel, '> el' (volgens modus ponens).
{X, (X A)}
A.
Voorbeeld ' el': (basisvorm):
(1) | A B;
(2) | A;
(3) | {* (1),(2), ' el' } B.
A)}
A.Voorbeeld '
el': (basisvorm):(1) | A
B;(2) | A;
(3) | {* (1),(2), '
el' } B.(4.2c)
Methode volgens Herbrand interpretatie.
Een klassieke variant van de reductiemethode is 'Herbrand logica' (J. Herbrand, 1931). Hierbij wordt uitsluitend van domeininterpretaties gebruik gemaakt waarbij alle variabelen worden vervangen door object constanten, zgn. ' grondsubstituties'.
{Zie o.a.:
Jacques Herbrand (1931): 'Sur la non-contradiction de l'arithmétique', Journal für die reine und angewandte Mathematik 166: pp.1-8, translated as 'On the consistency of arithmetic' in Van Heijenoort's 'From Frege to Godel'.}
Jacques Herbrand (1931): 'Sur la non-contradiction de l'arithmétique', Journal für die reine und angewandte Mathematik 166: pp.1-8, translated as 'On the consistency of arithmetic' in Van Heijenoort's 'From Frege to Godel'.}
Voorbeelden.
Zie hieronder, (4.2d) 'Methode van Minimaal domein definitie'.
(4.2d)
Methode van Minimaal domein definitie.
Een praktische combinatie van Convergente reductiemethode en Herbrand interpretatie, die geschikt is voor predikatenlogica, vind je in de Minimaal domein definitie bewijsmethode.
Voorbeelden.
Modus ponens (MP), in PDL
; Existentieel normaal vorm'.
D.w.z. met factieve premisse (referent) existentieel.
F1: {(
x (A[1](x)
B[1](x)) 
x A[1](x) };
F2: (x B[1](x) };
F1 [DNF] ={(x (¬A[1](x) B[1](x
)) x A[1](x) };
F1(M!): [DNF(Intens.)] ={((¬A1
F1(M!): DNF(Extens.)] ={((¬A1
={(¬A1
={((¬A1), (¬A2
={(¬A1, ¬A2, A1)
F1(M!): [DNF(Reduc.)] ={ (B1, ¬A2, A1)
F2(M!): [DNF(Intens.)] ={(By[c])};
F2(M!): [DNF(Extens.)] ={(B1
F1(M!), de premisse,
bestaat uit 8 componenten/disjuncten van elk 3 conjuncten, vier hiervan blijken te elimineren; de resterende vier
impliceren de conclusie, F2(M!).
x (A[1](x)
B[1](x)) x A[1](x) };
F2: (x B[1](x) };F1 [DNF] ={(
x (¬A[1](x) B[1](x
)) x A[1](x) };F1(M!): [DNF(Intens.)] ={((¬A1
/
B1), (¬A2/
B2)), (Ax[c]) };F1(M!): DNF(Extens.)] ={((¬A1
/
B1), (¬A2/
B2)), ((A1)/
(A2)) };={(¬A1
/
B1), (¬A2/
B2), (A1))/
(¬A1/
B1), (¬A2/
B2), (A2)) };={((¬A1), (¬A2
/
B2), (A1))/
((B1), (¬A2/
B2), (A1))/
((¬A1), (¬A2/
B2), (A2))/
((B1), (¬A2/
B2), (A2)) };={(¬A1, ¬A2, A1)
/
(¬A1, (B2, A1)/
(B1, ¬A2, A1)/
(B1, B2, A1)/
(¬A1, ¬A2, A2)/
(¬A1, B2, A2)/
(B1, ¬A2, A2)/
(B1, B2, A2) };F1(M!): [DNF(Reduc.)] ={ (B1, ¬A2, A1)
/
(B1, B2, A1)/
(¬A1, B2, A2)/
(B1, B2, A2) };F2(M!): [DNF(Intens.)] ={(By[c])};
F2(M!): [DNF(Extens.)] ={(B1
/
B2) };F1(M!), de premisse,
bestaat uit 8 componenten/disjuncten van elk 3 conjuncten, vier hiervan blijken te elimineren; de resterende vier
impliceren de conclusie, F2(M!).(4.2e)
Methode van Semantische tableaux
Oftewel Tableaumethode, boomdiagram-methode.
Toetsing van de geldigheid van een redenering door weerlegging van de onvervulbaarheid van het tegendeel.
Met name wordt onderzocht of er contradictie schuilt tussen de premisse(n) en het tegendeel van de conclusie. Voor dit doel worden de premisse(n) en de negatie van de conclusie tezamen in een conjunctief normaal vorm gebracht, waarna de disjuncties worden uitgesplitst in hun disjuncten, een 'tak' per disjunct. De bedoeling is om in de complementaire conclusie minstens één conjunct te vinden waarvan elke disjuncte 'tak' strijdig is met elke disjuncte 'tak' van minstens één conjunct in de premisse(n). In dat geval blijkt contradictie tussen conjuncten van complementaire conclusie en van premisse(n). Daarmee is onvervulbaarheid van het tegendeel aangetoond, dus geldigheid van de te toetsen bewering.
{Zie o.a.:
Evert W. Beth, 1959, 'The foundations of mathematics. A study in the philosophy of science'. Ophelders, Willy (W.M.J.), 'Automated theorem proving based upon a tableau-method with unification under restrictions. Theory, implementation and results'. Proefschrift (KUB, Tilburg), 5-6-1992: p.14.}
Evert W. Beth, 1959, 'The foundations of mathematics. A study in the philosophy of science'. Ophelders, Willy (W.M.J.), 'Automated theorem proving based upon a tableau-method with unification under restrictions. Theory, implementation and results'. Proefschrift (KUB, Tilburg), 5-6-1992: p.14.}
(4.2f)
Resolutie.
Deze methode is gebaseerd op het principe van toetsing van de te bewijzen redenering via weerlegging van het tegendeel, door het afleiden van een uitzondering of tegenvoorbeeld van het tegendeel. (reductio ad absurdum). Ook hier worden de premisse(n) en de negatie van de conclusie tezamen in een conjunctief normaal vorm gebracht. Hieruit wordt vervolgens een verzameling van kwantor-vrije, Skolem-normaal conjuncten afgeleid (de clause set). Doel is afleiding van minstens één lege verzameling conjuncten op de hoofdlijn van redenering, uit complementair e conjuncten in conclusie en in premisse(n). Van elk van die conjuncten is minstens één consequentie, afgeleide of interpretatie nodig. Hierbij kan gebruik worden gemaakt van regels voor reductie, resolutie en (in
PDL
-I) unificatie.{Zie o.m. Davis & Putnam (1960), John Alan Robinson (1965), N.J. Nilsson (1980),
Alexander A. Leitsch (1997).}
{Zie ook:
Bewijsmethode voor Predikatenlogica: Inleiding Resolutielogica .
En meer daarover: de Resolutiemethode (uitgebreid). }
Bewijsmethode voor Predikatenlogica: Inleiding Resolutielogica .
En meer daarover: de Resolutiemethode (uitgebreid). }
Voorbeelden.
Bewijs via resolutie (in PPL
).
Gegeven formule R:
R = {((A B) A)
B }.
Modus ponens.
Implicatie Eliminatie regel, '> el'.
Bewijs via resolutie:
Formule R is resolutie-beslisbaar geldig.
R = {((A
B) A)
B }.Modus ponens.
Implicatie Eliminatie regel, '> el'.
Bewijs via resolutie:
•
S ≡ ¬R;
S = {¬(((A B) A)
B) }.
Formule S is beslist onvervulbaar.
Aanname van het tegendeel S:
S ≡ ¬R;S = {¬(((A B) A)
B) }.•
· Negatief normaal vorm;
· Conjunctief normaal vorm:
{((A B)
A) ¬B };
{(¬A B) A
¬B }.
· Clausule Normaal Vorm:
{ 1:A, 2:¬B, 3:(¬A B) }.
Sluit (in contradictie).
Normaal vorm conversies:
· Negatief normaal vorm;
· Conjunctief normaal vorm:
{((A B)
A) ¬B };{(¬A B) A
¬B }.{ 1:A, 2:¬B, 3:(¬A B) }.•
Pad (a):
{1,3} 4:B; {2,4} 5:
.
Pad (b):
{1,3} 4:¬A; {1,4} 5:
.
Reductie(s):
Pad (a):
{1,3}
4:B; {2,4} 5:
.Pad (b):
{1,3}
4:¬A; {1,4} 5:
.Sluit (in contradictie).Formule S is beslist onvervulbaar.Formule R is resolutie-beslisbaar geldig.