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 the First Order Theory of Real Addition with Order
• A decision procedure for (co)datatypes in SMT solvers
• 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 Verification Conditions Using Satisfiability Modulo Theories
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving quantified linear arithmetic by counterexample-guided instantiation
• 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

Cited in

(11)

• Incremental determinization for quantifier elimination and functional synthesis
• On solving quantified bit-vector constraints using invertibility conditions
• E-matching for fun and profit
• Solving hard Mizar problems with instantiation and strategy invention
• Syntax-guided synthesis with quantitative syntactic objectives
• Quantifier instantiation techniques for finite model finding in SMT
• Tools and Algorithms for the Construction and Analysis of Systems
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Revisiting enumerative instantiation
• Synthesis of domain specific CNF encoders for bit-vector solvers

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)