Kvazirozhodovací procedury pro logické teorie reálných funkcí
Cíle projektu
Rozhodovací procedury pro teorie v predikátové logice hrají čím dál větší roli v informatice, zejména v kombinaci 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 teorií. Nejsou ale nejsou téměř žádné výsledky pro případ 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 patří vyhýbání se takovým případům 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é.
Klíčová slova
decision proceduresEntscheidungsproblemdecidabilitypredicate logicreal numbersreal functions
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
SGA0202100005
Hlavní účastníci
Ústav informatiky AV ČR, v. v. i.
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
21-09458S
Alternativní jazyk
Název projektu anglicky
Quasi-Decision Procedures for First-Order Theories of Real Functions
Anotace anglicky
Decision procedures for predicate logical theories play an increasingly important role in computer science, especially in combination with Boolean satisfiability solvers, that is, in the form of SAT modulo theory (SMT) solvers. While there is a vast amount of current research on decision procedures for integers, real numbers, arrays, and many other theories, there is almost no results for the case of real functions, although such functions play a fundamental role in many areas of computer science and mathematics. We conjecture that the reason for this situation is the difficulty of the problem which we propose to overcome by designing so-called quasi-decision procedures for real functions. A quasi-decision procedure relaxes the decision problem in such a way that it is not required to terminate in borderline cases where the satisfiability of the input formula changes under small perturbations of this formula. In many applications, such borderline cases are actively avoided, and hence quasi-decision procedures can solve precisely the cases that are important in such applications
Vědní obory
Kategorie VaV
ZV - Základní výzkum
OECD FORD - hlavní obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - vedlejší obor
—
OECD FORD - další vedlejší obor
—
CEP - odpovídající obory
(dle převodníku)AF - Dokumentace, knihovnictví, práce s informacemi
BC - Teorie a systémy řízení
BD - Teorie informace
IN - Informatika
Termíny řešení
Zahájení řešení
1. 4. 2021
Ukončení řešení
31. 3. 2024
Poslední stav řešení
—
Poslední uvolnění podpory
29. 2. 2024
Dodání dat do CEP
Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP25-GA0-GA-R
Datum dodání záznamu
12. 3. 2025
Finance
Celkové uznané náklady
2 541 tis. Kč
Výše podpory ze státního rozpočtu
2 541 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Uznané náklady
2 541 tis. Kč
Statní podpora
2 541 tis. Kč
0%
Poskytovatel
Grantová agentura České republiky
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Doba řešení
01. 04. 2021 - 31. 03. 2024