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_____%2F25%3A00616949" target="_blank" >RIV/67985807:_____/25:00616949 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/s10817-024-09716-3" target="_blank" >https://doi.org/10.1007/s10817-024-09716-3</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10817-024-09716-3" target="_blank" >10.1007/s10817-024-09716-3</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 augmented with trigonometric and exponential functions (NTA), however, there is no known direct representation of satisfying assignments that allows for a simple independent check of whether the represented numbers exist and satisfy the given formula. Hence, in this paper, we introduce a different form of satisfiability certificate for NTA, and formulate the satisfiability problem as the problem of searching for such a certificate. This does not only ease the independent verification of satisfiability, but also allows the design of new algorithms that show satisfiability by systematically searching for such certificates. Computational experiments document that the resulting algorithms are able to prove satisfiability of a substantially higher number of benchmark problems than existing methods. We also characterize the formulas whose satisfiability can be demonstrated by such a certificate, by providing lower and upper bounds in terms of relevant well-known classes. Finally we show the existence of a procedure for checking the satisfiability of NTA-formulas that terminates for formulas that satisfy certain robustness assumptions.

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 augmented with trigonometric and exponential functions (NTA), however, there is no known direct representation of satisfying assignments that allows for a simple independent check of whether the represented numbers exist and satisfy the given formula. Hence, in this paper, we introduce a different form of satisfiability certificate for NTA, and formulate the satisfiability problem as the problem of searching for such a certificate. This does not only ease the independent verification of satisfiability, but also allows the design of new algorithms that show satisfiability by systematically searching for such certificates. Computational experiments document that the resulting algorithms are able to prove satisfiability of a substantially higher number of benchmark problems than existing methods. We also characterize the formulas whose satisfiability can be demonstrated by such a certificate, by providing lower and upper bounds in terms of relevant well-known classes. Finally we show the existence of a procedure for checking the satisfiability of NTA-formulas that terminates for formulas that satisfy certain robustness assumptions.

Druh

J_ost - Ostatní články v recenzovaných periodicích

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í

2025

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 periodika

Journal of Automated Reasoning

ISSN

0168-7433

e-ISSN

1573-0670

Svazek periodika

69

Číslo periodika v rámci svazku

January 2025

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

35

Strana od-do

3

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—