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
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Skolemization for Substructural Logics Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Constrained Term Rewriting tooL

verfasst von : Cynthia Kop, Naoki Nishida

Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

This paper discusses Ctrl, a tool to analyse – both automatically and manually – term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and automatically analyse various properties such as termination, confluence and quasi-reductivity. Ctrl also offers both a manual and automatic mode for equivalence tests using inductive theorem proving, giving support for and verification of “hand-written” term equivalence proofs.

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 Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
Nächstes Kapitel Proof Search in Nested Sequent Calculi
Fußnoten
1
However, to avoid ambiguity in the input parser, the brackets and individual strings in the input file may not use the protected symbols [, , and ;, or spaces.
 
2
This failure is not unlikely, as constrained reduction following [11] requires validity of quantified formulas \(\exists \mathbf {x} [\varphi (\mathbf {x})]\), which is hard for most solvers. To improve performance, Ctrl uses default choices for \(\mathbf {x}\); this method is omitted here for space reasons.
 
3
The translation for integer transition systems uses a variation of Marc Brockschmidt’s SMT-Pushdown tool at https://​github.​com/​mmjb/​SMTPushdown.
 
Literatur
1.
de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) CrossRef
2.
Falke, S., Kapur, D.: A term rewriting approach to the automated termination analysis of imperative programs. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 277–293. Springer, Heidelberg (2009) CrossRef
3.
Falke, S., Kapur, D.: Rewriting Induction + Linear arithmetic = Decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 241–255. Springer, Heidelberg (2012) CrossRef
4.
Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Schmidt-Schauß, M. (ed.) Proc. RTA 2011. LIPIcs, vol. 10, pp. 41–50. Dagstuhl (2011)
5.
Furuichi, Y., Nishida, N., Sakai, M., Kusakari, K., Sakabe, T.: Approach to procedural-program verification based on implicit induction of constrained term rewriting systems. IPSJ Trans. Program. 1(2), 100–121 (2008). In Japanese
6.
Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving Termination of Programs Automatically with AProVE. In: Kapur, D., Weidenbach, C., Demri, S. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 184–191. Springer, Heidelberg (2014)
7.
Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(2), 71–739 (2011)CrossRef
8.
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (2006)MATHMathSciNetCrossRef
9.
Kop, C.: Termination of LCTRSs. In: Waldmann, J. (ed.) Proceedings of WST, pp. 59–63 (2013)
10.
Kop, C., Nishida, N.: Term Rewriting with Logical Constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 343–358. Springer, Heidelberg (2013) CrossRef
11.
Kop, C., Nishida, N.: Automatic constrained rewriting induction towards verifying procedural programs. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 334–353. Springer, Heidelberg (2014)
12.
13.
Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Lynch, C. (ed.) Proc. RTA 2010. LIPIcs, vol. 6, pp. 259–276. Dagstuhl (2010)
14.
Reddy, U.S: Term rewriting induction. In: Stickel, M. (ed.) Proc. CADE 1990. LNCS, vol. 449, pp. 162–177. Springer, Heidelberg (1990)
Metadaten
Titel
Constrained Term Rewriting tooL
verfasst von
Cynthia Kop
Naoki Nishida
Copyright-Jahr
2015
Verlag
Springer Berlin Heidelberg
Buch
Logic for Programming, Artificial Intelligence, and Reasoning

Print ISBN: 978-3-662-48898-0

Electronic ISBN: 978-3-662-48899-7

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-662-48899-7_38

Premium Partner

    Bildnachweise