Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
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 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
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
Others
Publication year
2023
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
NASA Formal Methods: 15th International Symposium, NFM 2023 Proceedings
ISBN
978-3-031-33169-5
ISSN
0302-9743
e-ISSN
—
Number of pages
17
Pages from-to
472-488
Publisher name
Springer
Place of publication
Cham
Event location
Houston
Event date
May 16, 2023
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—