Syntax-guided quantifier instantiation

DOI10.1007/978-3-030-72013-1_8MaRDI QIDQ2233503zbMATH OpenOpenAlexFDO

Authors Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-72013-1_8

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Formalization of mathematics in connection with theorem provers (68V20)

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

Cites work

• A decision procedure for (co)datatypes in SMT solvers
• A Decision Procedure for the First Order Theory of Real Addition with Order
• An abstract decision procedure for satisfiability in the theory of recursive data types
• Applying Linear Quantifier Elimination
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
• Counterexample-Guided Model Synthesis
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Datatypes with shared selectors
• Efficient E-Matching for SMT Solvers
• Efficiently solving quantified bit-vector formulas
• On solving quantified bit-vector constraints using invertibility conditions
• Quantifier instantiation techniques for finite model finding in SMT
• Revisiting enumerative instantiation
• Simplify: a theorem prover for program checking
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• 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. Procee

Cited in

(15)

• Counterexample-guided quantifier instantiation for synthesis in SMT
• On solving quantified bit-vector constraints using invertibility conditions
• Revisiting enumerative instantiation
• Synthesis of domain specific CNF encoders for bit-vector solvers
• E-matching for fun and profit
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Quantifier instantiation techniques for finite model finding in SMT
• Tools and Algorithms for the Construction and Analysis of Systems
• Syntax-guided synthesis with quantitative syntactic objectives
• Incremental determinization for quantifier elimination and functional synthesis
• Solving hard Mizar problems with instantiation and strategy invention
• SMT and functional equation solving over the reals: challenges from the IMO
• Machine learning for quantifier selection in cvc5
• The QSMA algorithm for quantifiers in SMT
• Negated string containment is decidable

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)