Bevis computing

Evidensbaseret databehandling er målrettet databehandling på en computer , kombineret med analytisk forskning, som fører til streng etablering af nye fakta og bevis for teoremer [1] .

Pålidelig databehandling

En af de hyppigt anvendte metoder til evidensbaserede beregninger er pålidelige beregninger. Pålidelige beregninger forstås som numeriske metoder med automatisk verifikation af nøjagtigheden af de opnåede resultater [2] . Ganske ofte er evidensbaserede beregninger baseret på intervalanalyse , hvor der i stedet for reelle tal tages i betragtning intervaller , der bestemmer værdiernes nøjagtighed. Intervalanalyse er meget brugt til beregninger med garanteret nøjagtighed i form af maskinaritmetik .

Eksempler

I talteori

På grund af det faktum, at talteori i høj grad opererer med heltal, viser brugen af demonstrative beregninger i talteori sig at være meget frugtbar.

Mersenne-tallet siges at være primtal . Det er teoretisk muligt for en person at kontrollere dette faktum , men praktisk talt kun ved brug af computerteknologi. $M_{{43112609}}=2^{{43112609}}-1$
L. Euler antog , at ligningen ikke har nogen løsninger i positive heltal. Det blev dog senere vist, at der er mindst én løsning: ${\displaystyle x_{1}^{5}+x_{2}^{5}+x_{3}^{5}+x_{4}^{5}=x_{5}^{5))$

x_{1}=27

, , , . _

x_{2}=84

x_{3}=110

x_{4}=133

x_{5}=144

Desuden blev denne løsning fundet ved hjælp af opregning på computeren [1] .

I grafteori

En af de mest berømte succeser i anvendelsen af evidensbaseret beregning i grafteori er løsningen af firefarveproblemet . Dette berømte problem blev stillet i 1852 og er formuleret som følger: "find ud af, om ethvert kort placeret på en kugle kan farves med fire farver, så to områder, der har en fælles del af grænsen, farves i forskellige farver." I 1976 viste K. Appel og W. Haken ved hjælp af evidensbaserede beregninger, at ethvert kort kan farvelægges på denne måde.

I hydrodynamik

Anvendelsen af evidensbaserede beregninger i matematiske problemer inden for hydrodynamik blev systematisk behandlet på Institut for Anvendt Matematik. M. V. Keldysh fra det russiske videnskabsakademi under ledelse af K. I. Babenko . Et eksempel er følgende sætning opnået ved hjælp af bevisberegninger [3] .

Sætning . For og Orr-Sommerfeld- spektralproblemet har en egenværdi , der ligger i halvplanet . Derfor er Poiseuille-flowet ustabilt i den lineariserede formulering for disse parametre . $\alpha =1.02$ $R=6000$ $\mathrm {Re} \,\lambda >0$

Flere eksempler

Booles problem med Pythagoras tripler .
Klassificering af Johnson polyedre .

Se også

Noter

↑ 1 2 Babenko K. I. . Grundlæggende om numerisk analyse. — M .: Nauka, 1986.
↑ Kulish W., Ratz D., Hammer R., Hawks M. Reliable Computing. Grundlæggende numeriske metoder. - RHD, 2005.
↑ Babenko K. I., Vasiliev M. M. Om proof-of-work-beregninger i problemet med stabiliteten af Poiseuille-strømmen // Dokl. - 1983. - T. 273 , nr. 6 . - S. 1289-1294 .

Litteratur

Pankov P.S. Bevisbaserede beregninger på elektroniske computere. - Frunze: Ilim, 1978. - 179 s.
K. I. Babenko. Om bevisberegninger og matematiske eksperiment på computer // Uspekhi Mat . - 1985. - T. 40 , nr. 4 (244) . - S. 137-138 .
Babenko K.I., Petrovich V.Yu., Rakhmanov A.I. Om et demonstrativt eksperiment i teorien om overfladebølger med endelig amplitude // Dokl. AN. . - 1988. - T. 303 , nr. 5 . - S. 1033-1037 .