First-Order Instantiation using Discriminating Terms
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00353736" target="_blank" >RIV/68407700:21730/21:00353736 - isvavai.cz</a>
Result on the web
<a href="http://sat.inesc-id.pt/~mikolas/discrsmt.pdf" target="_blank" >http://sat.inesc-id.pt/~mikolas/discrsmt.pdf</a>
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
First-Order Instantiation using Discriminating Terms
Original language description
This paper proposes a technique to limit the number of possible terms to be considered in quantifier instantiation. One of the major hurdles that SMT solvers face when dealing with quantifiers is that there are simply too many terms to instantiate with. So even if the right set of terms is available to the solver, meaning they appear in the formula, the solver might not have enough resources to come upon the right combination. This motivates the technique presented in this paper, which instantiates only by a certain type of terms, called discriminating terms. The paper introduces a class of formulas, where the proposed technique has a considerable impact.
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/LL1902" target="_blank" >LL1902: Powering SMT Solvers by Machine Learning</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2021
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
Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021)
ISBN
—
ISSN
1613-0073
e-ISSN
1613-0073
Number of pages
6
Pages from-to
17-22
Publisher name
CEUR Workshop Proceedings
Place of publication
Aachen
Event location
Los Angeles
Event date
Jul 18, 2021
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—