Deciding local theory extensions via E-matching

DOI10.1007/978-3-319-21668-3_6zbMath1381.68280arXiv1508.06827OpenAlexW1895616280MaRDI QIDQ1702888

Thomas Wies, Clark Barrett, Tim King, Kshitij Bansal, Andrew Reynolds

Publication date: 1 March 2018

Full work available at URL: https://arxiv.org/abs/1508.06827

Mathematics Subject Classification ID

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

Related Items (5)

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Separation logic with one quantified variable ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants

Uses Software

• Dafny
• Why3
• z3
• StarExec
• UFO
• GRASShopper
• H-PILoT

This page was built for publication: Deciding local theory extensions via E-matching