Syntax-guided quantifier instantiation
type: Item
instance of: scholarly article
title: Syntax-guided quantifier instantiation
zbMATH Open document ID: 1474.68456
DOI: 10.1007/978-3-030-72013-1_8
author: Aina Niemetz
author: Mathias Preiner
author: Andrew Reynolds
author: Clark Barrett
author: Cesare Tinelli
publication date: 2021-10-18T00:00:00Z
Mathematics Subject Classification ID: 68V20
Mathematics Subject Classification ID: 68T20
zbMATH DE Number: 7410484
MaRDI profile type: Publication
full work available at URL: 978-3-030-72013-1 8
OpenAlex ID: W3138477645
cites work: An abstract decision procedure for satisfiability in the theory of recursive data types
cites work: Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
cites work: Simplify: a theorem prover for program checking
cites work: A Decision Procedure for the First Order Theory of Real Addition with Order
cites work: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
cites work: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
cites work: Applying Linear Quantifier Elimination
cites work: Efficient E-Matching for SMT Solvers
cites work: Q2479551
cites work: On solving quantified bit-vector constraints using invertibility conditions
cites work: Solving SAT and SAT Modulo Theories
cites work: Counterexample-Guided Model Synthesis
cites work: Revisiting enumerative instantiation
cites work: A Decision Procedure for (Co)datatypes in SMT Solvers
cites work: Counterexample-guided quantifier instantiation for synthesis in SMT
cites work: Solving quantified linear arithmetic by counterexample-guided instantiation
cites work: Quantifier Instantiation Techniques for Finite Model Finding in SMT
cites work: Datatypes with shared selectors
cites work: Efficiently solving quantified bit-vector formulas
description: scientific article