Todistuslaskenta

Todistuspohjainen laskenta  on määrätietoista laskentaa tietokoneella yhdistettynä analyyttiseen tutkimukseen, joka johtaa uusien tosiasioiden tiukkaan vahvistamiseen ja lauseiden todistamiseen [1] .

Luotettavaa laskentaa

Yksi usein käytetyistä näyttöön perustuvien laskelmien menetelmistä on luotettavat laskelmat. Luotettavat laskelmat ymmärretään numeerisina menetelminä , joissa saatujen tulosten tarkkuus varmistetaan automaattisesti [2] . Varsin usein näyttöön perustuvat laskelmat perustuvat intervallianalyysiin , jossa reaalilukujen sijaan huomioidaan arvojen tarkkuuden määrääviä intervalleja . Intervallianalyysiä käytetään laajalti laskelmissa, joissa konearitmeettinen tarkkuus on taattu .

Esimerkkejä

Lukuteoriassa

Koska lukuteoria toimii suurelta osin kokonaislukujen kanssa, demonstratiivisten laskelmien käyttö lukuteoriassa osoittautuu erittäin hedelmälliseksi.

• Mersennen numeron sanotaan olevan alkuluku . Ihmisen on teoriassa mahdollista tarkistaa tämä tosiasia , mutta käytännössä vain tietotekniikan avulla.
• L. Euler oletti , että yhtälöllä ei ole ratkaisuja positiivisina kokonaislukuina. Myöhemmin kuitenkin osoitettiin, että on olemassa ainakin yksi ratkaisu:

Lisäksi tämä ratkaisu löydettiin tietokoneella suoritetun numeroinnin avulla [1] .

Graafiteoriassa

Yksi tunnetuimmista onnistumisista näyttöön perustuvan laskennan soveltamisessa graafiteoriassa on neliväriongelman ratkaisu . Tämä kuuluisa ongelma esitettiin vuonna 1852, ja se on muotoiltu seuraavasti: "Ota selvää, voidaanko mikä tahansa pallolla oleva kartta värittää neljällä värillä niin, että mitkä tahansa kaksi aluetta, joilla on yhteinen rajan osa, värjätään eri väreillä." Vuonna 1976 K. Appel ja W. Haken osoittivat näyttöön perustuvia laskelmia käyttäen, että mikä tahansa kartta voidaan värittää tällä tavalla.

Hydrodynamiikassa

Näyttöön perustuvien laskelmien käyttöä hydrodynamiikan matemaattisissa ongelmissa käsiteltiin systemaattisesti sovelletun matematiikan instituutissa. M. V. Keldysh Venäjän tiedeakatemiasta K. I. Babenkon johdolla . Esimerkkinä on seuraava todistuslaskelmien avulla saatu lause [3] .

Lause . For ja Orr-Sommerfeldin spektriongelmalla on ominaisarvo, joka sijaitsee puolitasossa . Siksi näiden parametrien linearisoidussa formulaatiossa Poiseuille-virtaus on epävakaa.

Lisää esimerkkejä

• Boolen ongelma Pythagoraan kolmiosissa .
• Johnson-polyhedran luokitus .

Katso myös

• Matemaattinen todiste
• kokeellinen matematiikka

Muistiinpanot

1. ↑ 1 2 Babenko K. I. . Numeerisen analyysin perusteet. - M .: Nauka, 1986.
2. ↑ Kulish W., Ratz D., Hammer R., Hawks M. Reliable Computing. Numeeriset perusmenetelmät. - RHD, 2005.
3. ↑ Babenko K. I., Vasiliev M. M. Todistuslaskelmista Poiseuillen virtauksen stabiiliuden ongelmassa // Dokl. - 1983. - T. 273 , nro 6 . - S. 1289-1294 .

Linkit

• Intervallianalyysi ja sen sovellukset

Kirjallisuus

• Pankov P.S. Todistuspohjaiset laskelmat elektronisilla tietokoneilla. - Frunze: Ilim, 1978. - 179 s.
• K. I. Babenko. Todistuslaskelmista ja matemaattisesta kokeesta tietokoneella  // Uspekhi Mat . - 1985. - T. 40 , nro 4 (244) . - S. 137-138 .
• Babenko K.I., Petrovich V.Yu., Rakhmanov A.I. Demonstratiivisesta kokeesta äärellisen amplitudin pinta-aaltojen teoriassa // Dokl. AN. . - 1988. - T. 303 , nro 5 . - S. 1033-1037 .