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
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 2/2018

11.03.2017

Many-Sorted Equivalence of Shiny and Strongly Polite Theories

verfasst von: Filipe Casal, João Rasga

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2018

Einloggen

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

search-config
loading …

Abstract

Herein we close the question of the equivalence of shiny and strongly polite theories by establishing that, for theories with a decidable quantifier-free satisfiability problem, the set of many-sorted shiny theories coincides with the set of many-sorted strongly polite theories. Capitalizing on this equivalence, we obtain a Nelson–Oppen combination theorem for many-sorted shiny theories.
Vorheriger Artikel Visibly Linear Temporal Logic
Nächster Artikel A Formalization of Metric Spaces in HOL Light

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 "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

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
Fußnoten
1
A correctness proof of the method was presented by Tinelli and Harandi [15].
 
2
As in [10], we do not restrict Y to be the set of variables in \({\mathsf {s}}\textsf {-}{\mathsf {witness}}\) since this generality is needed to show Lemma A.2 and Theorem 3.7 of [10].
 
Literatur
1.
Areces, C., Fontaine, P.: Combining theories: the ackerman and guarded fragments. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Frontiers of Combining Systems. FroCoS 2011. Lecture Notes in Computer Science, vol. 6989. Springer, Berlin, Heidelberg (2011)
2.
Casal, F., Rasga, J.: Revisiting the equivalence of shininess and politeness. In: Proceedings of the Nineteenth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’2013), Volume 8312 of LNCS, pp. 198–212 (2013)
3.
Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: International Joint Conference on Automated Reasoning, pp. 122–136. Springer International Publishing (2014)
4.
Cox, D., Little, J., O’shea, D.: Ideals, Varieties, and Algorithms, vol. 3. Springer, New York (1992)CrossRefMATH
5.
Daskalakis, C., Karp, R.M., Mossel, E., Riesenfeld, S.J., Verbin, E.: Sorting and selection in posets. SIAM J. Comput. 40(3), 597–622 (2011)MathSciNetCrossRefMATH
6.
Enderton, H.B.: A Mathematical Introduction to Logic. Elsevier Science (2001)
7.
Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems. FroCoS 2009. Lecture Notes in Computer Science, vol. 5749. Springer, Berlin, Heidelberg (2009)
7.
8.
Hopcroft, J.E., Tarjan, R.E.: Efficient algorithms for graph manipulation [H] (Algorithm 447). Commun. ACM 16(6), 372–378 (1973)CrossRef
9.
Jovanović, D., Barrett, C.: Polite theories revisited. In: Proceedings of the Seventeenth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’2010), Volume 6397 of LNCS, pp. 402–416 (2010)
10.
Jovanović, D., Barrett, C.: Polite theories revisited. Technical Report TR2010-922, Department of Computer Science, New York University (2010)
11.
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)CrossRefMATH
12.
13.
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (FroCoS’2005), Volume 3717 of LNAI, pp. 48–64 (2005)
14.
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), Volume 3 of Applied Logic Series, pp. 103–119 (1996)
15.
Metadaten
Titel
Many-Sorted Equivalence of Shiny and Strongly Polite Theories
verfasst von
Filipe Casal
João Rasga
Publikationsdatum
11.03.2017
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 2/2018
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-017-9411-y

Weitere Artikel der Ausgabe 2/2018

Journal of Automated Reasoning 2/2018 Zur Ausgabe

OriginalPaper

A Formalization of Metric Spaces in HOL Light

OriginalPaper

Genetic Programming Proof Search Automatic Improvement

OriginalPaper

Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning

OriginalPaper

Visibly Linear Temporal Logic

Premium Partner

    Bildnachweise