Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 3/2022

05-05-2022

Polite Combination of Algebraic Datatypes

Authors: Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett

Published in: Journal of Automated Reasoning | Issue 3/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.
previous article Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols
next article Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
1
A preliminary version of this work was published in the proceedings of IJCAR 2020 [26]. The current article extends the original versions with complete proofs, as well as a discussion and results regarding existential theories (see Proposition 2). Additionally, Sect. 5 is extended to provide a more comprehensive treatment of axiomatizations for trees.
 
2
We note that in practice, the new variables in \( wtn (\phi )\) are assumed to be fresh not only with respect to \(\phi \), but also with respect to the formula from the second theory being combined.
 
Literature
1.
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4:1-4:51 (2009)MathSciNetCrossRef
2.
Baader, F., Snyder, W., Narendran, P., Schmidt-Schauß, M., Schulz, K.U.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 Volumes), pp. 445–532. Elsevier/MIT Press, New York (2001)CrossRef
3.
Barrett, C.W., Dill, D.L., Stump, A.: A generalization of shostak’s method for combining decision procedures. In: A. Armando (ed.) Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8–10, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2309, pp. 132–146. Springer (2002)
4.
Barrett, C.W., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisfiab. Boolean Model. Comput. 3(1–2), 21–46 (2007)MathSciNetCrossRef
5.
6.
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). Available at www.​SMT-LIB.​org
7.
Berthon, R., Ringeissen, C.: Satisfiability modulo free data structures combined with bridging functions. In: T. King, R. Piskac (eds.) Proceedings of SMT@IJCAR 2016, CEUR Workshop Proceedings, vol. 1617, pp. 71–80. CEUR-WS.org (2016)
8.
Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. Electron. Notes Theor. Comput. Sci. 174(8), 55–70 (2007)CrossRef
9.
Bonacina, M.P., Fontaine, P., Ringeissen, C., Tinelli, C.: Theory combination: Beyond equality sharing. In: C. Lutz, U. Sattler, C. Tinelli, A. Turhan, F. Wolter (eds.) Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 11560, pp. 57–89. Springer (2019)
10.
Casal, F., Rasga, J.: Many-sorted equivalence of shiny and strongly polite theories. J. Autom. Reason. 60(2), 221–236 (2018)MathSciNetCrossRef
11.
Chocron, P., Fontaine, P., Ringeissen, C.: Politeness and combination methods for theories with bridging functions. J. Autom. Reason. 64(1), 97–134 (2020)MathSciNetCrossRef
12.
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (2001)MATH
13.
Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: S. Ghilardi, R. Sebastiani (eds.) Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16–18, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5749, pp. 263–278. Springer (2009)
14.
Gutiérrez, R., Meseguer, J.: Variant-based decidable satisfiability in initial algebras with predicates. In: F. Fioravanti, J.P. Gallagher (eds.) Logic-Based Program Synthesis and Transformation—27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10–12, 2017, Revised Selected Papers, Lecture Notes in Computer Science, vol. 10855, pp. 306–322. Springer (2017)
15.
Hojjat, H., Rümmer, P.: Deciding and interpolating algebraic data types by reduction. In: T. Jebelean, V. Negru, D. Petcu, D. Zaharie, T. Ida, S.M. Watt (eds.) 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, September 21–24, 2017, pp. 145–152. IEEE Computer Society (2017)
16.
Jovanovic, D., Barrett, C.W.: Polite theories revisited. In: C.G. Fermüller, A. Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6397, pp. 402–416. Springer (2010). Extended technical report is available at http://​theory.​stanford.​edu/​~barrett/​pubs/​JB10-TR.​pdf
17.
Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: G. Castagna, A.D. Gordon (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017, pp. 260–270. ACM (2017)
18.
19.
Krstic, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: O. Grumberg, M. Huth (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24–April 1, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4424, pp. 602–617. Springer (2007)
20.
Manna, Z., Zarba, C.G.: Combining decision procedures. In: B.K. Aichernig, T.S.E. Maibaum (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18–20, 2002, Revised Papers, Lecture Notes in Computer Science, vol. 2757, pp. 381–422. Springer (2002)
21.
Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program. 154, 3–41 (2018)CrossRef
22.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)CrossRef
23.
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: B. Gramlich (ed.) Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19–21, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3717, pp. 48–64. Springer (2005). Extended technical report is available at https://​hal.​inria.​fr/​inria-00070335/​
24.
Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. J. Autom. Reason. 58(3), 341–362 (2017)MathSciNetCrossRef
25.
Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C.W.: Datatypes with shared selectors. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Lecture Notes in Computer Science, vol. 10900, pp. 591–608. Springer (2018)
26.
Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.W.: Politeness for the theory of algebraic datatypes. In: IJCAR (1), Lecture Notes in Computer Science, vol. 12166, pp. 238–255. Springer (2020)
27.
Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C.W., Tinelli, C.: Politeness and stable infiniteness: Stronger together. In: CADE, Lecture Notes in Computer Science, vol. 12699, pp. 148–165. Springer (2021)
28.
29.
Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: R.A. Schmidt (ed.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2–7, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5663, pp. 67–83. Springer (2009)
30.
Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. J. Autom. Reason. 30(1), 1–31 (2003)MathSciNetCrossRef
31.
Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: J.J. Alferes, J.A. Leite (eds.) Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27–30, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3229, pp. 641–653. Springer (2004)
32.
33.
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)MathSciNetCrossRef
Metadata
Title
Polite Combination of Algebraic Datatypes
Authors
Ying Sheng
Yoni Zohar
Christophe Ringeissen
Jane Lange
Pascal Fontaine
Clark Barrett
Publication date
05-05-2022
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 3/2022
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09625-3

Other articles of this Issue 3/2022

Journal of Automated Reasoning 3/2022 Go to the issue

OriginalPaper

Combination of Uniform Interpolants via Beth Definability

OriginalPaper

Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols

EditorialNotes

Special Issue of Selected Extended Papers of IJCAR 2020

OriginalPaper

The Resolution of Keller’s Conjecture

OriginalPaper

Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains

Premium Partner

    Image Credits