Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic Kapitel lesen Erstes Kapitel lesen

2017 | Supplement | Buchkapitel

Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case)

verfasst von : Silvio Ghilardi, Alessandro Gianola

Erschienen in: Frontiers of Combining Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In this paper, we study the conditions under which existence of interpolants (for quantifier-free formulae) is modular, in the sense that it can be transferred from two first-order theories \(T_1, T_2\) to their combination \(T_1 \cup T_2\). We generalize to the non-disjoint signatures case the results from [3]. As a surprising application, we relate the Horn combinability criterion of this paper to superamalgamability conditions known from propositional logic and we use this fact to derive old and new results concerning fusions transfer of interpolation properties in modal logic.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Merging Fragments of Classical Logic
Nächstes Kapitel The Boolean Solution Problem from the Perspective of Predicate Logic
Fußnoten
1
Notice that in the above definition free function and predicate symbols (not already present in the signature \(\varSigma \) of T) are not allowed; allowing them (and requiring that only shared symbols occur in the interpolant \(\theta \)) produces a different stronger definition, which is nevertheless reducible to quantifier-free interpolation in the combination with the theory of equality with uninterpreted function symbols (see [3]).
 
2
It is possible to characterize syntactically strong sub-amalgamability in terms of a suitable ‘equality interpolating’ condition [3]. That sub-amalgamability needs to be strenghtened to strong sub-amalgamability in order to get positive combination results is demonstrated by converse facts also proved in [3].
 
3
It is not difficult to realize (using well-known Löwenheim-Skolem theorems [4]) that one can get all the results in the paper by limiting this definition to forks among structures whose cardinality is bounded by the cardinality of set of the formulae in our signatures (signatures are finite or countable in all practical cases).
 
4
We can freely assume that \(ELEM_L^{\mathcal {M}_{1}}\cap ELEM_L^{\mathcal {M}_{2}}=ELEM_L^{\mathcal {A}} \) and \(LIST^{\mathcal {M}_{1}}\cap LIST^{\mathcal {M}_{2}}=LIST^{\mathcal {A}} \).
 
5
BAO stands for ‘Boolean algebras with operators’.
 
6
We recall that in every Boolean algebra (more generally, in every semilattice) \(x\le y\) is defined as \(x\cap y=x\), where \(\cap \) is the meet operation.
 
Literatur
1.
Bacsich, P.D.: Amalgamation properties and interpolation theorems for equational theories. Algebra Universalis 5, 45–55 (1975)MathSciNetCrossRefMATH
2.
Bruttomesso, R., Ghilardi, S., Ranise, S.: From strong amalgamability to modularity of quantifier-free interpolation. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 118–133. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-31365-3_​12 CrossRef
3.
Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1), 5:1–5:34 (2014)
4.
Chang, C.-C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland, Amsterdam-London (1990)MATH
5.
Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22, 269–285 (1957)MathSciNetCrossRefMATH
6.
7.
Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (extended version). Technical report (2017)
8.
9.
Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. ACM Trans. Comput. Logic 9(2), 1–54 (2008)CrossRefMATH
10.
Henzinger, T., McMillan, K.L., Jhala, R., Majumdar, R.: Abstractions from Proofs. In: POPL, pp. 232–244 (2004)
11.
Kapur, D., Majumdar, R., Zarba, C.: Interpolation for data structures. In: SIGSOFT’06/FSE-14, pp. 105–116 (2006)
12.
Maksimova, L.L.: Craig’s theorem in superintuitionistic logics and amalgamable varieties. Algebra i Logika 16(6), 643–681, 741 (1977)
13.
Maksimova, L.L.: Interpolation theorems in modal logics and amalgamable varieties of topological Boolean algebras. Algebra i Logika 18(5), 556–586, 632 (1979)
14.
Maksimova, L.L.: Interpolation theorems in modal logics. Sufficient conditions. Algebra i Logika 19(2), 194–213, 250–251 (1980)
15.
16.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Programm. Lang. Syst. 1(2), 245–257 (1979)CrossRefMATH
17.
18.
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data structures with arithmetic constraints: a non-disjoint combination. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 319–334. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-04222-5_​20 CrossRef
19.
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Satisfiability procedures for combination of theories sharing integer offsets. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 428–442. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-00768-2_​35 CrossRef
20.
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)MathSciNetMATH
21.
Segerberg, K.: An Essay in Classical Modal Logic, Filosofiska Studier, vol. 13. Uppsala Universitet (1971)
22.
23.
Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 273–289. Springer, Cham (2016). doi:10.​1007/​978-3-319-40229-1_​19
24.
Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proceedings of FroCoS 1996, Applied Logic, pp. 103–120. Kluwer Academic Publishers (1996)
25.
26.
Wolter, F.: Fusions of modal logics revisited. In Advances in Modal Logic, vol. 1 (Berlin, 1996), CSLI Lecture Notes, pp. 361–379 (1998)
27.
Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 353–368. Springer, Heidelberg (2005). doi:10.​1007/​11532231_​26 CrossRef
Metadaten
Titel
Interpolation, Amalgamation and Combination (The Non-disjoint Signatures Case)
verfasst von
Silvio Ghilardi
Alessandro Gianola
Copyright-Jahr
2017
Buch
Frontiers of Combining Systems

Print ISBN: 978-3-319-66166-7

Electronic ISBN: 978-3-319-66167-4

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66167-4_18

Premium Partner

    Bildnachweise