Počet záznamů: 1  

Quasi-Decidability of a Fragment of the First-Order Theory of Real Numbers

  1. 1.
    0449388 - ÚI 2017 RIV NL eng J - Článek v odborném periodiku
    Franek, Peter - Ratschan, Stefan - Zgliczynski, P.
    Quasi-Decidability of a Fragment of the First-Order Theory of Real Numbers.
    Journal of Automated Reasoning. Roč. 57, č. 2 (2016), s. 157-185. ISSN 0168-7433. E-ISSN 1573-0670
    Grant CEP: GA ČR GCP202/12/J060; GA MŠMT OC10048; GA ČR GA15-14484S
    Institucionální podpora: RVO:67985807
    Klíčová slova: decidability * decision procedure * real numbers
    Kód oboru RIV: IN - Informatika
    Impakt faktor: 1.636, rok: 2016

    In this paper we consider a fragment of the first-order theory of the real numbers that includes systems of n equations in n variables, and for which all functions are computable in the sense that it is possible to compute arbitrarily close interval approximations. Even though this fragment is undecidable, we prove that - under the additional assumption of bounded domains-there is a (possibly non-terminating) algorithm for checking satisfiability such that (1) whenever it terminates, it computes a correct answer, and (2) it always terminates when the input is robust. A formula is robust, if its satisfiability does not change under small continuous perturbations. We also prove that it is not possible to generalize this result to the full first-order language - removing the restriction on the number of equations versus number of variables. As a basic tool for our algorithm we use the notion of degree from the field of topology.
    Trvalý link: http://hdl.handle.net/11104/0250958

     
    Název souboruStaženoVelikostKomentářVerzePřístup
    a0449388.pdf9702.4 KBVydavatelský postprintvyžádat
     
Počet záznamů: 1  

  Tyto stránky využívají soubory cookies, které usnadňují jejich prohlížení. Další informace o tom jak používáme cookies.