Syntax-guided quantifier instantiation
From MaRDI portal
Publication:2233503
DOI10.1007/978-3-030-72013-1_8zbMATH Open1474.68456OpenAlexW3138477645MaRDI QIDQ2233503FDOQ2233503
Authors: Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli 
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-72013-1_8
Recommendations
- Counterexample-Guided Model Synthesis
- Quantifier instantiation techniques for finite model finding in SMT
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Solving quantified verification conditions using satisfiability modulo theories
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Simplify: a theorem prover for program checking
- Efficiently solving quantified bit-vector formulas
- A Decision Procedure for the First Order Theory of Real Addition with Order
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- A decision procedure for (co)datatypes in SMT solvers
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Quantifier instantiation techniques for finite model finding in SMT
- Applying Linear Quantifier Elimination
- 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
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Revisiting enumerative instantiation
- Solving quantified linear arithmetic by counterexample-guided instantiation
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Datatypes with shared selectors
- On solving quantified bit-vector constraints using invertibility conditions
- Counterexample-Guided Model Synthesis
Cited In (11)
- Tools and Algorithms for the Construction and Analysis of Systems
- Syntax-guided synthesis with quantitative syntactic objectives
- Synthesis of domain specific CNF encoders for bit-vector solvers
- On solving quantified bit-vector constraints using invertibility conditions
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Revisiting enumerative instantiation
- Quantifier instantiation techniques for finite model finding in SMT
- Solving hard Mizar problems with instantiation and strategy invention
- E-matching for fun and profit
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Incremental determinization for quantifier elimination and functional synthesis
This page was built for publication: Syntax-guided quantifier instantiation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233503)
