Revisiting enumerative instantiation
From MaRDI portal
Publication:2324227
DOI10.1007/978-3-319-89963-3_7zbMath1423.68468OpenAlexW2795154181MaRDI QIDQ2324227
Pascal Fontaine, Andrew Reynolds, Haniel Barbosa
Publication date: 16 September 2019
Full work available at URL: https://doi.org/10.1007/978-3-319-89963-3_7
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (15)
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Quantifier simplification by unification in SMT ⋮ Unifying splitting ⋮ Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving ⋮ Syntax-guided quantifier instantiation ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ A unifying splitting framework ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Extending SMT solvers to higher-order logic ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ SAT-Inspired Eliminations for Superposition
This page was built for publication: Revisiting enumerative instantiation
