Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)
Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. JSAT 3(1–2), 21–46 (2007)
Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) 24th International Conference on Automated Deduction (CADE-24), Lake Placid, NY, USA, volume 7898 of LNCS, pp. 39–57. Springer (2013)
Chocron, P., Fontaine, P., Ringeissen, C.: A Gentle non-disjoint combination of satisfiability procedures. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proceedings of the 7th International Joint Conference on Automated Reasoning, IJCAR, volume 8562 of LNCS, pp. 122–136. Springer (2014)
Chocron, P., Fontaine, P., Ringeissen, C.: A polite non-disjoint combination method: theories with bridging functions revisited. In: Felty, A.P., Middeldorp, A. (eds.) 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, volume 9195 of LNCS, pp. 419–433. Springer (2015)
Chocron, P., Fontaine, P., Ringeissen, C.: A rewriting approach to the combination of data structures with bridging theories. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems (FroCoS), volume 9322 of LNCS, pp. 275–290. Springer (2015)
Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’04), volume 3452 of LNCS, pp. 51–66. Springer (2005)
Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3–4), 221–249 (2004)
Jovanovic, D., Barrett, C.: Polite theories revisited. In: Fermueller, C., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’10), volume 6397 of LNCS, pp. 402–416. Springer (2010)
Kruglov, E., Weidenbach, C.: Superposition decides the first-order logic fragment over ground theories. Math. Comput. Sci. 6(4), 427–456 (2012)
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combinable extensions of Abelian groups. In: Schmidt, R.A. (ed.) 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, volume 5663 of LNCS, pp. 51–66. Springer (2009)
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combining satisfiability procedures for unions of theories with a shared counting operator. Fundam. Inform. 105(1–2), 163–187 (2010)
Oppen, D.C.: Reasoning about recursively defined data structures. J. ACM 27(3), 403–411 (1980)
Pham, T., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. J. Autom. Reason. 57(4), 281–318 (2016)
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) Frontiers of Combining Systems (FroCoS), volume 3717 of LNCS, pp. 48–64. Springer (2005)
Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351–360 (1979)
Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, volume 5663 of LNCS, pp. 67–83. Springer (2009)
Sofronie-Stokkermans, V.: Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms. In: Ball, T., Giesl, J., Hähnle, R., Nipkow, T. (eds.) Interaction versus Automation: The Two Faces of Deduction, number 09411 in Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Germany (2010)
Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: Hermenegildo, M.V., Palsberg, J. (eds.) Principles of Programming Languages (POPL), pp. 199–210. ACM, New York (2010)
Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) 18th International Symposium on Static Analysis (SAS), Venice, Italy, volume 6887 of LNCS, pp. 298–315. Springer (2011)
Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. J. Autom. Reason. 30(1), 1–31 (2003)
Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson–Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems (FroCoS). Applied Logic, pp. 103–120. Kluwer Academic Publishers, Dordrecht (1996)
Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1), 291–353 (2003)
Tran, D., Ringeissen, C., Ranise, S., Kirchner, H.: Combination of convex theories: modularity, deduction completeness, and explanation. J. Symb. Comput. 45(2), 261–286 (2010)
Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems (FroCoS), volume 5749 of LNCS, pp. 366–382. Springer (2009)
Zarba, C.G.: Combining lists with integers. In: International Joint Conference on Automated Reasoning (Short Papers), Technical Report DII 11/01, pp. 170–179. University of Siena (2001)
Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) 18th International Conference on Automated Deduction (CADE-18), Copenhagen, Denmark, volume 2392 of LNCS, pp. 363–376. Springer (2002)
Zarba, C.G.: Combining sets with cardinals. J. Autom. Reason. 34(1), 1–29 (2005)
Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. Inf. Comput. 204(10), 1526–1574 (2006)
