Deciding Predicate Logical Theories Of Real-Valued Functions

0579461 - ÚI 2024 RIV DE eng C - Konferenční příspěvek (zahraniční konf.)
Ratschan, Stefan
Deciding Predicate Logical Theories Of Real-Valued Functions.
48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023 - (Leroux, J.; Lombardy, S.; Peleg, D.), č. článku 76. Leibniz International Proceedings in Informatics, 272. ISBN 978-3-95977-292-1. ISSN 1868-8969.
[MFCS 2023: International Symposium on Mathematical Foundations of Computer Science /48./. Bordeaux (FR), 28.08.2023-01.09.2023]
Grant CEP: GA ČR(CZ) GA21-09458S
Institucionální podpora: RVO:67985807
Klíčová slova: decision procedures * first-order predicate logical theories * real numbers * real-valued functions
Obor OECD: Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
https://doi.org/10.4230/LIPIcs.MFCS.2023.76

The notion of a real-valued function is central to mathematics, computer science, and many other scientific fields. Despite this importance, there are hardly any positive results on decision procedures for predicate logical theories that reason about real-valued functions. This paper defines a first-order predicate language for reasoning about multi-dimensional smooth real-valued functions and their derivatives, and demonstrates that – despite the obvious undecidability barriers – certain positive decidability results for such a language are indeed possible.
Trvalý link: https://hdl.handle.net/11104/0348265


Vědecká data: ArXiv.org (preprint)