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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
History and Prospects for First-Order Automated Deduction Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems

verfasst von : Kiraku Shintani, Nao Hirokawa

Erschienen in: Automated Deduction - CADE-25

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present a confluence tool for left-linear term rewrite systems. The tool proves confluence by using Hindley’s commutation theorem together with three commutation criteria, including Church-Rosser modulo associative and/or commutative theories. Despite a small number of its techniques, experiments show that the tool is comparable to recent powerful confluence tools.

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 Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent
Nächstes Kapitel Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies
Fußnoten
2
All problems and results are available at the tool website (see the URL in Section 1).
 
Literatur
1.
Hindley, J.R.: The Church-Rosser Property and a Result in Combinatory Logic. Ph.D. thesis, University of Newcastle-upon-Tyne (1964)
2.
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
3.
Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)MathSciNetCrossRefMATH
4.
5.
6.
Schulz, K.: Word unification and transformation of generalized equations. In: Abdulrab, H., Pecuchet, J.-P. (eds.) IWWERT 1991. LNCS, vol. 677, pp. 150–176. Springer, Heidelberg (1993) CrossRef
7.
Schmidt, R.A.: \(E\)-Unification for subsystems of \(S4\). In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 106–120. Springer, Heidelberg (1998) CrossRef
8.
9.
Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 93–102. Springer, Heidelberg (2009) CrossRef
10.
Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)MathSciNetCrossRefMATH
11.
Toyama, Y.: Commutativity of term rewriting systems. In: Fuchi, K., Kott, L. (eds.) Programming of Future Generation Computers II, pp. 393–407. North-Holland, Amsterdam (1988)
12.
13.
van Oostrom, V.: Confluence by decreasing diagrams. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 306–320. Springer, Heidelberg (2008) CrossRef
14.
Aoto, T.: Automated confluence proof by decreasing diagrams based on rule-labelling. In: Lynch, C. (ed.) RTA 2010, LIPIcs, vol. 6, pp. 7–16 (2010)
15.
Pottier, L.: Minimal solutions of linear diophantine systems: bounds and algorithms. In: Book, R.V. (ed.) Rewriting Techniques and Applications. LNCS, vol. 488, pp. 162–173. Springer, Heidelberg (1991)CrossRef
16.
Ohlebusch, E.: Modular Properties of Composable Term Rewriting Systems. Ph.D. thesis, Universität Bielefeld (1994)
17.
Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI – a confluence tool. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE-23. LNCS, vol. 6803, pp. 499–505. Springer, Heidelberg (2011) CrossRef
18.
19.
Durán, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational maude specifications. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69–85. Springer, Heidelberg (2010) CrossRef
20.
Aoto, T., Toyama, Y.: A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. LMCS 8(1), 1–29 (2012)MathSciNet
21.
Metadaten
Titel
CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
verfasst von
Kiraku Shintani
Nao Hirokawa
Copyright-Jahr
2015
Buch
Automated Deduction - CADE-25

Print ISBN: 978-3-319-21400-9

Electronic ISBN: 978-3-319-21401-6

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-21401-6_8