Abstract
The Nelson-Oppen method [4] allows the combination of satisfiability procedures of stably infinite theories with disjoint signatures. Due to its importance, several attempts to extend the method to different and wider classes of theories were made. In 2005, it was shown that shiny [9] and polite [6] theories could be combined with an arbitrary theory (the relationship between these classes was analysed in [6]). Later, a stronger notion of polite theory was proposed, see [3], in order to overcome a subtle issue with a proof in [6]. In this paper, we analyse the relationship between shiny and strongly polite theories in the onesorted case. We show that a shiny theory with a decidable quantifier-free satisfiability problem is strongly polite and provide two different sufficient conditions for a strongly polite theory to be shiny. Based on these results, we derive a combination method for the union of a polite theory with an arbitrary theory.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)
Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012)
Jovanović, D., Barrett, C.: Polite theories revisited. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 402–416. Springer, Heidelberg (2010)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Oppen, D.C.: Complexity, convexity and combinations of theories. Theoretical Computer Science 12, 291–302 (1980)
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 48–64. Springer, Heidelberg (2005)
Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proceedings of the First International Workshop on Frontiers of Combining Systems (FroCoS 1996). Applied Logic Series, vol. 3, pp. 103–119 (1996)
Tinelli, C., Harandi, M.T.: Constraint logic programming over unions of constraint theories. Journal of Functional and Logic Programming 1998(6) (1998)
Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. Journal of Automated Reasoning 34(3), 209–238 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Casal, F., Rasga, J. (2013). Revisiting the Equivalence of Shininess and Politeness. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)