{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:24Z","timestamp":1776333384155,"version":"3.51.2"},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>SMT solvers can decide the satisfiability of ground formulas modulo a combination of<\/jats:p><jats:p>built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures.<\/jats:p><jats:p>In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate using the theory of arrays, how such proofs can be achieved in our formalism.<\/jats:p>","DOI":"10.29007\/3c1n","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:11Z","timestamp":1516730351000},"page":"22-11","source":"Crossref","is-referenced-by-count":8,"title":["Reasoning with Triggers"],"prefix":"10.29007","volume":"20","author":[{"given":"Claire","family":"Dross","sequence":"first","affiliation":[]},{"given":"Sylvain","family":"Conchon","sequence":"additional","affiliation":[]},{"given":"Johannes","family":"Kanig","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Paskevich","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"SMT 2012. 10th International Workshop on Satisfiability Modulo Theories"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T17:59:12Z","timestamp":1516730352000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/27L"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/3c1n","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}],"subject":[]}}