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

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

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

Original language description

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.

Czech name

—

Czech description

—

Type

J_ost - Miscellaneous article in a specialist periodical

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/GA21-09458S" target="_blank" >GA21-09458S: Quasi-Decision Procedures for First-Order Theories of Real Functions</a><br>

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2025

Confidentiality

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

Name of the periodical

Journal of Automated Reasoning

ISSN

0168-7433

e-ISSN

1573-0670

Volume of the periodical

69

Issue of the periodical within the volume

January 2025

Country of publishing house

DE - GERMANY

Number of pages

35

Pages from-to

3

UT code for WoS article

—

EID of the result in the Scopus database

—