Bewijsvoering met computer(software)

[Bartjes]

Opmerking moderator

Afgesplitst vanuit dit topic.

Ik vraag mij al een tijdje af of het handig zou zijn een (online?) programma te gebruiken om (tegen)bewijzen te zoeken voor de theorie (formele en metaformele getallen) waar ik aan werk.

- Is het doenlijk door een dergelijk programma eigen bedenksels te laten uitproberen zonder dat je er meer tijd in moet steken om het programma te laten begrijpen wat de bedoeling is dan het aan tijdsbesparing oplevert?

- Wat zijn de ervaringen van professionele wiskundigen met zulke programma's als hulpmiddel bij theorieontwikkeling?

[Xenion]

Mijn ervaringen met wiskundige software zijn beperkt tot Derive en MATLAB, maar jij wil je computer laten redeneren. Ik denk dat je dan eerder op zoek moet gaan naar logische programmeertalen (bv prolog).

Daar kan je bv enkele gekende regels invoeren en dan controleren of je hypotheses kunnen afgeleid worden uit die regels.

Of misschien dat je hier toch een programma vindt dat je kan gebruiken.

[Bartjes]

@ Xenion

Dank. Het gaat mij vooral om de vraag of het de moeite loont, je moet immers eerst zo'n taal leren en dan is het nog de vraag of het programma met bruikbare resultaten komt. Dus zeg maar het kosten/baten plaatje.

Verder bestaan er zoveel programma's dat ik niet meer weet wat hierin wijsheid is. Stel dat iemand al ervaring met een specifiek programma heeft, dan kan ik daarvan leren wat me te wachten staat.

[Xenion]

Mja het hangt ervan af wat je concreet wil bereiken. Kan je een voorbeeld geven?

[Bartjes]

http://sciencetalk.nl/forum/index.php/topic/176550-nieuwe-poging/page__pid__920822#entry920822

Hier ben ik nu al een hele tijd mee aan het worstelen.

[Xenion]

Ik weet niet hoe flexibel die programma's zijn op die wikipedia pagina die ik gaf want ik ken ze zelf niet.

Ik denk dat je met prolog wel dingen kan bereiken. De cursus declaratief programmeren die ik dit jaar gevolg heb gebruikte 'Simply logical: intelligent reasoning by example' als referentiewerk. Dat is gratis online beschikbaar.

Logica zal je al wel kennen, maar je zou eens moeten doornemen hoe het juist in de taal geïmplementeerd is, want de bewijsvoering gebeurt depth first met backtracking.

Je moet de gekende stellingen opgeven als 'facts' en dan kan je vragen om op basis van die regels zaken te bewijzen.

[Bartjes]

Ik zal eerst dat boek 'Simply logical: intelligent reasoning by example' eens doornemen.

[eezacque]

Wiskunde is onvolledig, bewijsbaarheid is onbeslisbaar. Ik heb nog geen stellingbewijzer mogen ontmoeten die praktisch bruikbaar is...

[Xenion]

Je hebt gelijk dat het in het algemeen niet zal kunnen, maar Bartjes is bezig met een soort eigen getallensysteem op te stellen. Als die regels telkens neergeschreven worden, dan kan je normaal wel een computer laten controleren of een nieuwe hypothese die jij voorstelt wel degelijk kan afgeleid worden uit de bestaande regels. Dat zou mogelijk wel tijd en moeite kunnen sparen.

[Bartjes]

Je hebt gelijk dat het in het algemeen niet zal kunnen, maar Bartjes is bezig met een soort eigen getallensysteem op te stellen. Als die regels telkens neergeschreven worden, dan kan je normaal wel een computer laten controleren of een nieuwe hypothese die jij voorstelt wel degelijk kan afgeleid worden uit de bestaande regels. Dat zou mogelijk wel tijd en moeite kunnen sparen.

Inderdaad. Ook als bepaalde zaken onbewijsbaar zijn, kan je een programma in principe wel alle mogelijke bewijzen laten uitproberen. Zo komt er dan een steeds groter reservoir aan bewezen stellingen beschikbaar. Slimme programma's kunnen wellicht ook gericht zoeken. De wiskunde is na Gödels stellingen ook niet tot stilstand gekomen. En voor bewijs-programma's hoeft dat evenmin te gelden.

Een andere kwestie is of zulke programma's – in mijn geval – praktisch nuttig zijn, daar ben ik nog niet uit.

[eezacque]

De wiskunde is na Gödels stellingen ook niet tot stilstand gekomen. En voor bewijs-programma's hoeft dat evenmin te gelden.

Het is ook meer het domein van de informatica, en die heeft op dit punt in pak 'm beet een halve eeuw bar weinig opgeleverd...

[Bartjes]

Het is ook meer het domein van de informatica, en die heeft op dit punt in pak 'm beet een halve eeuw bar weinig opgeleverd...

Heb je daar een bron of link voor. Best mogelijk dat je gelijk hebt, maar ik wil dat wel graag natrekken.

[eezacque]

Wikipedia geeft een overzicht van de stand van zaken (http://en.wikipedia.org/wiki/Automated_theorem_proving), met een overzicht van bestaande software, maar ik zie geen systeem waar je zo even mee aan de slag kunt (ik ga me hier niet in verdiepen, maar niets weerhoudt je ervan hier wel werk van te maken) Een probleem is dat je systeem van formele getallen niet heel duidelijk gedefinieerd is, zo maak je gebruik van reele getallen die nou eenmaal niet zo eenvoudig te definieren zijn in huis- tuin- en keukenlogica.

[Tempus]

zo maak je gebruik van reele getallen die nou eenmaal niet zo eenvoudig te definieren zijn in huis- tuin- en keukenlogica.

Wat bedoel je met 'huis- tuin en keukenlogica'? Want met tweede orde logica kan je de reële getallen karakertizeren tot aan isomorfie. Zie ook hier.

[eezacque]

Met huis- tuin- en keukenlogica bedoel ik eerste orde predicaatlogica. In deze logica is geautomatiseerd stellingbewijzen een slangenkuil, in tweede orde logica wil je er niet eens over nadenken.