Generalizations of shininess improve theory combination methods
Two generalizations of shininess
Logic in Computer Science
Summary
Combining different types of logical theories helps computers solve complicated problems more efficiently. Shininess is one such method used in this combination process. The authors introduce two new broader ways to generalize shininess, making it easier to work with theories that don’t meet previous strict requirements. This helps understand and improve existing methods, and they also compare their new approaches to older ones to show their strengths.
What this means in practice
- •For software verification engineers: Improve algorithms that combine different decision procedures for verifying software correctness by using broader shininess generalizations.
- •For automated reasoning developers: Design solvers that handle a wider range of theories without strict smoothness or computability constraints using the new generalizations of shininess.
A theory result. No direct application yet.
Authors
Guilherme V. Toledo, Yoni Zohar
Abstract
Shininess is one of the main theory combination methods in Satisfiability Modulo Theories. We present two infinite families of generalizations of it: one involving a property between gentleness and shininess, which helps us see gentleness itself as a variation of shininess; and another having no further computability requirements on the weaker theory, in addition dropping the need for smoothness. We prove these methods sharp, and compare them with existing methods.