Quasi-Decision Procedures for First-Order Theories of Real Functions
Project goals
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
Keywords
decision proceduresEntscheidungsproblemdecidabilitypredicate logicreal numbersreal functions
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
SGA0202100005
Main participants
Ústav informatiky AV ČR, v. v. i.
Contest type
VS - Public tender
Contract ID
21-09458S
Alternative language
Project name in Czech
Kvazirozhodovací procedury pro logické teorie reálných funkcí
Annotation in Czech
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é.
Scientific branches
R&D category
ZV - Basic research
OECD FORD - main branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - secondary branch
—
OECD FORD - another secondary branch
—
AF - Documentation, librarianship, work with information
BC - Theory and management systems
BD - Information theory
IN - Informatics
Solution timeline
Realization period - beginning
Apr 1, 2021
Realization period - end
Mar 31, 2024
Project status
—
Latest support payment
Feb 29, 2024
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP25-GA0-GA-R
Data delivery date
Mar 12, 2025
Finance
Total approved costs
2,541 thou. CZK
Public financial support
2,541 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Recognised costs
2 541 CZK thou.
Public support
2 541 CZK thou.
0%
Provider
Czech Science Foundation
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Solution period
01. 04. 2021 - 31. 03. 2024