Revisiting enumerative instantiation

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (17)

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 ⋮ Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version) ⋮ Solving hard Mizar problems with instantiation and strategy invention ⋮ 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