First-Order Instantiation using Discriminating Terms

Kód výsledku v 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>

Výsledek na webu

<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

—

Jazyk výsledku

angličtina

Název v původním jazyce

First-Order Instantiation using Discriminating Terms

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

First-Order Instantiation using Discriminating Terms

Popis výsledku anglicky

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.

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/LL1902" target="_blank" >LL1902: Obohacování SMT řešičů pomocí strojového učení</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

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

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

Počet stran výsledku

6

Strana od-do

17-22

Název nakladatele

CEUR Workshop Proceedings

Místo vydání

Aachen

Místo konání akce

Los Angeles

Datum konání akce

18. 7. 2021

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

WRD - Celosvětová akce

Kód UT WoS článku

—