Skip to main content
Registrieren
Springer Professional
SUCHE
MENÜ 1 2 3 4
nach oben

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Erschienen in: Journal of Automated Reasoning 3/2022

05.05.2022

Polite Combination of Algebraic Datatypes

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

Erschienen in: Journal of Automated Reasoning | Ausgabe 3/2022

Einloggen, um Zugang zu erhalten
share
TEILEN

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.
Vorheriger Artikel Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols
Nächster Artikel Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 69.000 Bücher
  • über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

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





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

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



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren
Fußnoten
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.
 
Literatur
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.
Krstic, S., Conchon, S.: Canonization for disjoint unions of theories. Inf. Comput. 199(1–2), 87–106 (2005) MathSciNetCrossRef
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.
Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351–360 (1979) MathSciNetCrossRef
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
Metadaten
Titel
Polite Combination of Algebraic Datatypes
verfasst von
Ying Sheng
Yoni Zohar
Christophe Ringeissen
Jane Lange
Pascal Fontaine
Clark Barrett
Publikationsdatum
05.05.2022
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 3/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09625-3

Weitere Artikel der Ausgabe 3/2022

Journal of Automated Reasoning 3/2022 Zur Ausgabe

OriginalPaper

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

EditorialNotes

Special Issue of Selected Extended Papers of IJCAR 2020

OriginalPaper

The Resolution of Keller’s Conjecture

OriginalPaper

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

OriginalPaper

Combination of Uniform Interpolants via Beth Definability

Premium Partner