beslisbaar

Beslisbaar is een term uit wiskunde en informatica die een eigenschap van een probleem beschrijft. Een probleem is beslisbaar als er een algoritme bestaat dat voor elke invoer precies één ja- of nee-uitkomst geeft en bij elk invoer onvermijdelijk stopt.

In de logica wordt een theorie beslisbaar genoemd wanneer er een procedure bestaat die voor elke formele uitspraak in die theorie beslist of die uitspraak geldig is (waar in alle modellen) of een uitspraak een theorema is. Meer algemeen verwijst beslisbaarheid naar het bestaan van een regelmatige beslissingsprocedure voor alle invoeren van een bepaald probleem.

Voorbeelden van beslisbare systemen zijn onder meer de Presburger-aritmetiek (getallen met optelling) en de theorie van reële gesloten velden (beslist door Tarski). Daartegen staat dat veel andere belangrijke theories en problemen onbeslisbaar zijn; een bekend voorbeeld is Peano-arithmetiek met optelling en vermenigvuldiging, en het halting-probleem, dat geen algemene beslissing procedure heeft die voor alle programma’s en invoeren halt maakt.

Beslissbaarheid is een eigenschap van een probleem op zich, los van de tijd die nodig is om het op te lossen. Een probleem kan decidable zijn maar extreem lang duren om op te lossen (niet-efficiënt), en daarmee praktisch onbruikbaar zijn. De term onderscheidt zich van de bredere notie van computabiliteit, waarbij soms ook gedeeltelijke algoritmen zonder gegarandeerde haltstellingen worden bestudeerd.

Zie ook beslissingsprobleem, recursieve verzamelingen en halting-probleem.

---