z-logo
open-access-imgOpen Access
Experimenting with Theory Instantiation in Vampire
Author(s) -
Martin Riener
Publication year - 2020
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/pf85
Subject(s) - computer science , satisfiability modulo theories , vampire , avatar , modulo , programming language , theory , theoretical computer science , discrete mathematics , mathematics , human–computer interaction
Theory instantiation tackles the problem of theory reasoning with quantifiers in Vam- pire using an SMT solver. In contrast to AVATAR modulo theories it works locally by instantiating a clause such that its pure theory part becomes inconsistent and can be deleted. We report on the challenges when adding instantiation for the theory of arrays.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.
Having issues? You can contact us here