Syntax-guided quantifier instantiation
From MaRDI portal
Publication:2233503
DOI10.1007/978-3-030-72013-1_8zbMath1474.68456OpenAlexW3138477645MaRDI QIDQ2233503
Clark Barrett, Aina Niemetz, Andrew Reynolds, Mathias Preiner, Cesare Tinelli
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-72013-1_8
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Datatypes with shared selectors
- On solving quantified bit-vector constraints using invertibility conditions
- Revisiting enumerative instantiation
- Efficiently solving quantified bit-vector formulas
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
- An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
- Applying Linear Quantifier Elimination
- Counterexample-Guided Model Synthesis
- A Decision Procedure for (Co)datatypes in SMT Solvers
- Solving SAT and SAT Modulo Theories
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- A Decision Procedure for the First Order Theory of Real Addition with Order
- Quantifier Instantiation Techniques for Finite Model Finding in SMT
This page was built for publication: Syntax-guided quantifier instantiation
