Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F23%3A00574098" target="_blank" >RIV/67985807:_____/23:00574098 - isvavai.cz</a>

Výsledek na webu

<a href="https://dx.doi.org/10.1007/978-3-031-33170-1_29" target="_blank" >https://dx.doi.org/10.1007/978-3-031-33170-1_29</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-33170-1_29" target="_blank" >10.1007/978-3-031-33170-1_29</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem

Popis výsledku v původním jazyce

For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satisfies the given formula. For non-linear real arithmetic with transcendental functions, however, no general finite representation of satisfying assignments is available. Hence, in this paper, we introduce a different form of satisfiability certificate for this theory, formulate the satisfiability verification problem as the problem of searching for such a certificate, and show how to perform this search in a systematic fashion. This does not only ease the independent verification of results, but also allows the systematic design of new, efficient search techniques. Computational experiments document that the resulting method is able to prove satisfiability of a substantially higher number of benchmark problems than existing methods.

Název v anglickém jazyce

Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem

Popis výsledku anglicky

For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satisfies the given formula. For non-linear real arithmetic with transcendental functions, however, no general finite representation of satisfying assignments is available. Hence, in this paper, we introduce a different form of satisfiability certificate for this theory, formulate the satisfiability verification problem as the problem of searching for such a certificate, and show how to perform this search in a systematic fashion. This does not only ease the independent verification of results, but also allows the systematic design of new, efficient search techniques. Computational experiments document that the resulting method is able to prove satisfiability of a substantially higher number of benchmark problems than existing methods.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA21-09458S" target="_blank" >GA21-09458S: Kvazirozhodovací procedury pro logické teorie reálných funkcí</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2023

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

NASA Formal Methods: 15th International Symposium, NFM 2023 Proceedings

ISBN

978-3-031-33169-5

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

17

Strana od-do

472-488

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Houston

Datum konání akce

16. 5. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—