Syntax-guided quantifier instantiation (Q2233503)

From MaRDI portal

Jump to:navigation, search

scientific article

Language	Label	Description	Also known as
English	Syntax-guided quantifier instantiation	scientific article

Statements

scholarly article

0 references

Syntax-guided quantifier instantiation (English)

0 references

0 references

Mathias Preiner

0 references

Andrew Reynolds

0 references

0 references

0 references

publication date

18 October 2021

0 references

MaRDI profile type

MaRDI publication profile

0 references

full work available at URL

https://doi.org/10.1007/978-3-030-72013-1_8

0 references

An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types

0 references

Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings

0 references

Simplify: a theorem prover for program checking

0 references

A Decision Procedure for the First Order Theory of Real Addition with Order

0 references

Solving Quantified Verification Conditions Using Satisfiability Modulo Theories

0 references

Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories

0 references

Applying Linear Quantifier Elimination

0 references

Efficient E-Matching for SMT Solvers

0 references

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

0 references

On solving quantified bit-vector constraints using invertibility conditions

0 references

Solving SAT and SAT Modulo Theories

0 references

Counterexample-Guided Model Synthesis

0 references

Revisiting enumerative instantiation

0 references

A Decision Procedure for (Co)datatypes in SMT Solvers

0 references

Counterexample-guided quantifier instantiation for synthesis in SMT

0 references

Solving quantified linear arithmetic by counterexample-guided instantiation

0 references

Quantifier Instantiation Techniques for Finite Model Finding in SMT

0 references

Datatypes with shared selectors

0 references

Efficiently solving quantified bit-vector formulas

0 references

Identifiers

zbMATH Open document ID

0 references

10.1007/978-3-030-72013-1_8

0 references

Mathematics Subject Classification ID

0 references

0 references

zbMATH DE Number

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:2233503

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q2233503&oldid=36722615"