Externí odkazy

Kvazirozhodovací procedury pro logické teorie reálných funkcí

GA21-09458S [Registrované výsledky] 2021 - 2024

Rozhodovací procedury pro teorie v predikátové logice hrají čím dále větší roli v informatice, zejména v kombinací s řešiči pro Boolovskou splnitelnost, tj. v SAT modulo teorie (SMT) řešičích. Existuje široké pole výzkumu rozhodovacích procedur pro celá čísla, reálná čísla, různé datové struktury a mnoho dalších teorii. Skoro ale nejsou žádné výsledky pro příklad reálných funkcí, ačkoli reálné funkce hrají fundamentální roli v mnoha oblastech informatiky a matematiky. Důvod pro tuto situaci je pravděpodobně těžkost problému. Tuto situaci chceme překonat tím, že místo rozhodovacích procedur chceme navrhnout kvazirozhodovací procedury pro reálné funkce. Kvazirozhodovací procedury zjednodušují problém tím, že nepožadují terminaci pro určité hraniční případy, kde infinitesimální změny vstupní formule změní i její splnitelnost. V mnoha aplikacích vyhýbání se takovým případům patří k základním postupům. Kvazirozhodovací procedury tudíž vyřeší přesné tyto případy, které jsou v takových aplikacích důležité.