Springen naar inhoud

Bewijsvoering met computer(software)


  • Log in om te kunnen reageren

#1

*_gast_Bartjes_*

  • Gast

Geplaatst op 05 augustus 2012 - 10:56

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?

Veranderd door Drieske, 06 augustus 2012 - 07:55


Dit forum kan gratis blijven vanwege banners als deze. Door te registeren zal de onderstaande banner overigens verdwijnen.

#2

Xenion

    Xenion


  • >1k berichten
  • 2606 berichten
  • Moderator

Geplaatst op 05 augustus 2012 - 11:26

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.

#3

*_gast_Bartjes_*

  • Gast

Geplaatst op 05 augustus 2012 - 12:34

@ 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.

#4

Xenion

    Xenion


  • >1k berichten
  • 2606 berichten
  • Moderator

Geplaatst op 05 augustus 2012 - 21:09

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

#5

*_gast_Bartjes_*

  • Gast

Geplaatst op 05 augustus 2012 - 21:15

http://www.wetenscha...822#entry920822

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

#6

Xenion

    Xenion


  • >1k berichten
  • 2606 berichten
  • Moderator

Geplaatst op 05 augustus 2012 - 21:44

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.

#7

*_gast_Bartjes_*

  • Gast

Geplaatst op 05 augustus 2012 - 22:26

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

#8

*_gast_eezacque_*

  • Gast

Geplaatst op 17 augustus 2012 - 04:24

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

#9

Xenion

    Xenion


  • >1k berichten
  • 2606 berichten
  • Moderator

Geplaatst op 17 augustus 2012 - 10:52

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.

#10

*_gast_Bartjes_*

  • Gast

Geplaatst op 17 augustus 2012 - 13:47

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.

#11

*_gast_eezacque_*

  • Gast

Geplaatst op 17 augustus 2012 - 15:39

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...

#12

*_gast_Bartjes_*

  • Gast

Geplaatst op 17 augustus 2012 - 15:58

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.

#13

*_gast_eezacque_*

  • Gast

Geplaatst op 17 augustus 2012 - 16:16

Wikipedia geeft een overzicht van de stand van zaken (http://en.wikipedia....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.

#14

Tempus

    Tempus


  • >250 berichten
  • 340 berichten
  • Ervaren gebruiker

Geplaatst op 17 augustus 2012 - 17:54

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.

#15

*_gast_eezacque_*

  • Gast

Geplaatst op 17 augustus 2012 - 18:09

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.





0 gebruiker(s) lezen dit onderwerp

0 leden, 0 bezoekers, 0 anonieme gebruikers

Ook adverteren op onze website? Lees hier meer!

Gesponsorde vacatures

Vacatures