8 papers
Automated Reasoning with Nested Datatypes
Tomer Hakak, Yoni Zohar, Andrew Reynolds +2
We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging.…
Bringing closure to theory combination properties
Guilherme V. Toledo, Benjamin Przybocki, Yoni Zohar
We consider the closure of three classical combination properties, namely, stable infiniteness, gentleness and shininess (or, equivalently for decidable theories, strong politeness…
Characterizing Sets of Theories That Can Be Disjointly Combined
Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar
We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describ…
Shininess, strong politeness, and unicorns
Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar
Shininess and strong politeness are properties related to theory combination procedures. In a paper titled "Many-sorted equivalence of shiny and strongly polite theories", Casal an…
Number theory combination: natural density and SMT
Guilherme V. Toledo, Yoni Zohar
The study of theory combination in Satisfiability Modulo Theories (SMT) involves various model theoretic properties (e.g., stable infiniteness, smoothness, etc.). We show that such…
Being polite is not enough (and other limits of theory combination)
Guilherme V. Toledo, Benjamin Przybocki, Yoni Zohar
In the Nelson-Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and th…