Cargando…
Syntax-Guided Quantifier Instantiation
This paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point ari...
Autores principales: | Niemetz, Aina, Preiner, Mathias, Reynolds, Andrew, Barrett, Clark, Tinelli, Cesare |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2021
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984542/ http://dx.doi.org/10.1007/978-3-030-72013-1_8 |
Ejemplares similares
-
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
por: Reynolds, Andrew, et al.
Publicado: (2020) -
The instantiation of values
por: Balazs, Zoltan
Publicado: (2013) -
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
por: Scott, Joseph, et al.
Publicado: (2021) -
Instantiating global crisis networks: The case of SARS
por: van Baalen, Peter J., et al.
Publicado: (2009) -
Cross-Cultural Differences and Similarities in Human Value Instantiation
por: Hanel, Paul H. P., et al.
Publicado: (2018)