Uoverensstemmelsen mellem matematiske beviser, algoritmer, og deres implementeringer i kontrolsystemer

Ingeniører arbejder i kvantificerbar realisme - et objekt eksisterer og kan måles. Sommetider, selvom, objektets sikkerhed og hvordan det vil opføre sig vakler. Forskere fra Automatic Control and System Dynamics Laboratory ved Technische Universität Chemnitz i Tyskland begynder at lukke kløften mellem virkelighed og matematisk usikkerhed.

De offentliggjorde en analyse af uoverensstemmelsen mellem matematiske beviser, algoritmer, og deres implementeringer i kontrolsystemer med reelle, målbare resultater. Deres arbejde vises i juli-udgaven af IEEE/CAA Journal of Automatica Sinica ( JAS ), en fælles udgivelse af IEEE og Chinese Association of Automation.

"Kontrolsystemer optræder i alt fra vaskemaskiner til raketter, sagde Pavel Osinenko, en forfatter på papiret. "Kontrolingeniører arbejder med objekter, der svarer til virkeligheden. For modeller af rigtige objekter, vi skal udvikle rigtige controllere, der fungerer i den endelige applikation. Klassisk matematik er god til at undersøge meget abstrakte objekter, men de overskrider kontrolteorien."

I klassisk matematisk teori, Osinenko sagde, styrke er en vigtig faktor, der kan gå glip af kontrolteoriens pointe. Styrke, I dette tilfælde, henviser til specificiteten af ​​de formidlede oplysninger. Nogle pattedyr er mennesker, og nogle mennesker er kvinder, og nogle kvinder er mødre. I klassisk matematik, det er stærkere at vide, at en variabel i en ligning er en menneskelig mor end blot et pattedyr, fordi der kan udledes flere oplysninger.

"For at kontrolteorien kan fungere, det kræver en logisk baggrund, der er langt svagere, "Osinenko sagde, bemærker, at klassisk matematik kræver et logisk system med flere trin for at sikre, at den mest specifikke information forbliver så stærk som muligt. "Vi har brug for et minimalistisk logisk system til kontrolteori."

Forskerne analyserede et hundrede år gammelt teorem af matematikeren Constantin Carathéodory. Sætningen hævder, at et problem med en foranderlig uafhængig variabel, såsom banen for en kastet bold, kan løses med svage logiske systemer.

"Det er konstruktiv matematik – ethvert objekt, som du kan konstruere eller bevise at eksisterer, kan beregnes. Du kan indtaste et matematisk bevis en til en i din computer, " sagde Osinenko.

Det er ikke tilfældet i klassisk matematik, hvor objekter ofte bevises ved at antage, at de ikke eksisterer, før modstridende matematik giver bevis.

Forskeren udforskede en variant af Caratheordorys teorem, der dækker flere problemer i praksis og ikke kun i teorien. Det er forbindelsen mellem teoremer og beviser og beregningssikkerhed.

"Klassisk matematik siger, at der er en sort kat i et mørkt rum. Den er bestemt derinde, men du kan ikke pege på dens præcise placering, " sagde Osinenko. "Dette minimale logiske system er faklen, som vi lyser rummet op med. Katten er lige der."

Forfatterne planlægger yderligere at undersøge minimale logiske systemer og konstruktiv matematik, med fokus på automatiseret ræsonnement for at hjælpe med løsninger til kontrolsystemer.

"Der er et hav af matematiske resultater og teorier i kontrolteori, som stadig venter på deres konstruktive behandling, " sagde Osinenko. "Det næste skridt er for os at vælge en og finde ud af det."