Abstract
Combining rewriting modulo an equational theory and SMT solving introduces new challenges in the area of term rewriting. One such challenge is unification of terms in the presence of equations and of uninterpreted and interpreted function symbols. The interpreted function symbols are part of a builtin model which can be reasoned about using an SMT solver. In this article, we formalize this problem, that we call unification modulo builtins. We show that under reasonable assumptions, complete sets of unifiers for unification modulo builtins problems can be effectively computed by reduction to usual E-unification problems and by relying on an oracle for SMT solving.
Author supplied keywords
Cite
CITATION STYLE
Ciobâcă, Ş., Arusoaie, A., & Lucanu, D. (2018). Unification modulo builtins. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10944 LNCS, pp. 179–195). Springer Verlag. https://doi.org/10.1007/978-3-662-57669-4_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
