Skip to Main content Skip to Navigation
New interface
Journal articles

Politeness and Combination Methods for Theories with Bridging Functions

Paula Chocron 1 Pascal Fontaine 2, 3 Christophe Ringeissen 4 
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
4 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : The Nelson-Oppen combination method is ubiquitous in Satisfiability Modulo Theories solvers. However, one of its major drawbacks is to be restricted to disjoint unions of theories. We investigate the problem of extending this combination method to particular non-disjoint unions of theories defined by connecting disjoint theories via bridging functions. A possible application is to solve verification problems expressed in a combination of data structures connected to arithmetic with bridging functions such as the length of lists and the size of trees. We present a sound and complete combination method à la Nelson-Oppen for the theory of absolutely free data structures, including lists and trees. This combination procedure is then refined for standard interpretations. The resulting theory has a nice politeness property, enabling combinations with arbitrary decidable theories of elements. In addition, we have identified a class of polite data structure theories for which the combination method remains sound and complete. This class includes all the subtheories of absolutely free data structures (e.g, the empty theory, injectivity, projection). Again, the politeness property holds for any theory in this class, which can thus be combined with bridging functions and arbitrary decidable theories of elements. This illustrates the significance of politeness in the context of non-disjoint combinations of theories.
Document type :
Journal articles
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Thursday, March 5, 2020 - 2:31:45 PM
Last modification on : Friday, July 8, 2022 - 10:07:49 AM
Long-term archiving on: : Saturday, June 6, 2020 - 3:18:23 PM


Files produced by the author(s)




Paula Chocron, Pascal Fontaine, Christophe Ringeissen. Politeness and Combination Methods for Theories with Bridging Functions. Journal of Automated Reasoning, 2020, 64, pp.97-134. ⟨10.1007/s10817-019-09512-4⟩. ⟨hal-01988452⟩



Record views


Files downloads