Characterizing Sets of Theories That Can Be Disjointly Combined
We study properties that allow first-order theories to be disjointly combined, including stable infiniteness, shininess, strong politeness, and gentleness. Specifically, we describe a Galois connection between sets of decidable theories, which picks out the largest set of decidable theories that can be combined with a given set of decidable theories. Using this, we exactly characterize the sets of decidable theories that can be combined with those satisfying well-known theory combination properties. This strengthens previous results and answers in the negative several long-standing open questions about the possibility of improving existing theory combination methods to apply to larger sets of theories. Additionally, the Galois connection gives rise to a complete lattice of theory combination properties, which allows one to generate new theory combination methods by taking meets and joins of elements of this lattice. We provide examples of this process, introducing new combination theorems. We situate both new and old combination methods within this lattice.
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:10 - 17:25 | |||
16:10 25mTalk | Characterizing Sets of Theories That Can Be Disjointly Combined POPL DOI | ||
16:35 25mTalk | Context-Free-Language Reachability for Almost-Commuting Transition Systems POPL Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison DOI | ||
17:00 25mTalk | Determination Problems for Orbit Closures and Matrix Groups POPL Rida Ait El Manssour University of Oxford, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS, Anton Varonka TU Wien, James Worrell University of Oxford DOI | ||