röksemdakerfi

Röksemdakerfi, eða sönnunarverkfæri í formlegri rökfræði, er formlegt kerfi sem gerir kleift að leiða staðhæfingar frá tilteknu safni axióma með reglum ályktunar. Kerfið inniheldur formlegt tungumál, axióma og reglur um ályktun. Sönnun er röð setninga þar sem hver setning er axióm eða afleiðing fyrri setninga með notkun reglna ályktunar.

Helstu gerðir röksemdakerfa eru t.d. Hilbert-stíll kerfi, sem notar fá axióma og eina aðalsreglu til að leiða nýjar setningar (ofta modus ponens); náttúruleg sönnun (natural deduction) með innleiðingar- og útlíkurreglum sem auðvelda byggingu sanna sannana; og sekventakerfi (sequent calculus) sem byggir á sequentum og reglur sem stuðla að réttri samröðun og niðurfellingu.

Eigindleikar röksemdakerfa eru réttmæti og fullkomnun: réttmæti (soundness) þýðir að allt sem er sannað í kerfinu er sannlegt í öllum túlkunum, en fullkomnun (completeness) þýðir að hvert réttanlegt ráðunaut (hægt að sannast fyrir öll túlkanir) sé sannað í kerfinu. Auk þess er mikilvægt fyrir rannsóknir og forritunarfræðingar að kerfin séu ákvörðunar- eða óvissubundin (decidable) í ákveðnum skiptum.

Saga og notkun: Röksemdakerfi hafa mótað stofnun stærðfræði og formgæðisfræði. Helstu fræðimenn eins og David Hilbert og Gerhard Gentzen mótuðu grunnreglur og kenningar um réttmæti, fullkomnun og útdrátt. Í dagNotkun kerfa kemur fram í tölvuverkfræði, formgæðum forrita og sönnunarverkfærum sem styðja við stærðfræðilegar sannanir og formlega staðfestingu forrita.