nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

CSI: New Evidence – A Progress Report

verfasst von : Julian Nagele, Bertram Felgenhauer, Aart Middeldorp

Erschienen in: Automated Deduction – CADE 26

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

CSI is a strong automated confluence prover for rewrite systems which has been in development since 2010. In this paper we report on recent extensions that make CSI more powerful, secure, and useful. These extensions include improved confluence criteria but also support for uniqueness of normal forms. Most of the implemented techniques produce machine-readable proof output that can be independently verified by an external tool, thus increasing the trust in CSI. We also report on CSI\(\mathbf {\hat{~}}\)oho, a tool built on the same framework and similar ideas as CSI that automatically checks confluence of higher-order rewrite systems.

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 DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL

Nächstes Kapitel Scalable Fine-Grained Proofs for Formula Processing

Available from http://coco.nue.riec.tohoku.ac.jp/2013, http://coco.nue.riec.tohoku.ac.jp/2014, http://coco.nue.riec.tohoku.ac.jp/2015, http://coco.nue.riec.tohoku.ac.jp/2016, under Entrants.

http://cops.uibk.ac.at.

http://cl-informatik.uibk.ac.at/software/mkbtt.

In fact, CSI uses a modified definition of \(\mathcal {S}^e\) that avoids adding extended rules for rules where the same linear variable appears as an argument of the two top-flattenings of the left-hand and right-hand sides of the rule, using the same AC symbol. In the example, this applies to the first two rules. We still have \({\rightarrow _{\mathcal {S}/\mathsf {AC}}} = {\rightarrow _{\mathcal {S}^e,\mathsf {AC}}} \cdot \sim _\mathsf {AC}\).

This can be shown using tree automata techniques [11].

A term is a pattern if free variables only have distinct bound variables as arguments.

A development step

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-63046-5_24/453657_1_En_24_IEq159_HTML.gif

contracts multiple, non-overlapping but possibly nested redexes at once.

IsaFoR/CeTA and CPF are available at http://cl-informatik.uibk.ac.at/software/ceta.

Full details are available from CSI’s website.

Aoto, T., Hirokawa, N., Nagele, J., Nishida, N., Zankl, H.: Confluence competition 2015. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 101–104. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_5 CrossRef

Aoto, T., Toyama, Y.: A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. LMCS 8(1: 31), 1–29 (2012). doi:10.2168/LMCS-8(1:31)2012 MathSciNetMATH

Aoto, T., Toyama, Y.: Ground confluence prover based on rewriting induction. In: Proceedings of 1st FSCD. LIPIcs, vol. 52, pp. 33: 1–33: 12 (2016). doi:10.4230/LIPIcs.FSCD.2016.33

Aoto, T., Toyama, Y., Uchida, K.: Proving confluence of term rewriting systems via persistency and decreasing diagrams. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 46–60. Springer, Cham (2014). doi:10.1007/978-3-319-08918-8_4

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). doi:10.1007/978-3-642-02348-4_7 CrossRef

Appel, C., van Oostrom, V., Simonsen, J.G.: Higher-order (non-)modularity. In: Proceedings of 21st RTA. LIPIcs, vol. 6, pp. 17–32 (2010). doi:10.4230/LIPIcs.RTA.2010.17

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)CrossRefMATH

Felgenhauer, B.: Deciding confluence of ground term rewrite systems in cubic time. In: Proceedings of 23rd RTA. LIPIcs, vol. 15, pp. 165–175 (2012). doi:10.4230/LIPIcs.RTA.2012.165

Felgenhauer, B.: Efficiently deciding uniqueness of normal forms and unique normalization for ground TRSs. In: Proceedings of 5th IWC, pp. 16–20 (2016)

10.

Felgenhauer, B., Middeldorp, A., Zankl, H., Oostrom, V.O.: Layer systems for proving confluence. ACM TOCL 16(2: 14), 1–32 (2015). doi:10.1145/2710017 MathSciNetCrossRefMATH

11.

Felgenhauer, B., Thiemann, R.: Reachability analysis with state-compatible automata. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 347–359. Springer, Cham (2014). doi:10.1007/978-3-319-04921-2_28 CrossRef

12.

Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. JACM 27(4), 797–821 (1980). doi:10.23638/LMCS-13(2:4)2017 MathSciNetCrossRefMATH

13.

Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986). doi:10.1137/0215084 MathSciNetCrossRefMATH

14.

Kahrs, S., Smith, C.: Non-\(\omega \)-overlapping TRSs are UN. In: Proceedings of 1st FSCD. LIPIcs, vol. 52, pp. 22: 1–22: 17 (2016). doi:10.4230/LIPIcs.FSCD.2016.22

15.

Klein, D., Hirokawa, N.: Confluence of non-left-linear TRSs via relative termination. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 258–273. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28717-6_21 CrossRef

16.

Klop, J.: Combinatory reduction systems. Ph.D. thesis, Utrecht University (1980)

17.

Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)

18.

Kop, C.: Higher order termination. Ph.D. thesis, Vrije Universiteit, Amsterdam (2012)

19.

Kusakari, K., Isogai, Y., Sakai, M., Blanqui, F.: Static dependency pair method based on strong computability for higher-order rewrite systems. IEICE TIS 92–D(10), 2007–2015 (2009)

20.

Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. TCS 192(1), 3–29 (1998). doi:10.1016/S0304-3975(97)00143-6 MathSciNetCrossRefMATH

21.

Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. JLP 1(4), 497–536 (1991). doi:10.1093/logcom/1.4.497 MathSciNetMATH

22.

Nagele, J., Felgenhauer, B., Middeldorp, A.: Improving automatic confluence analysis of rewrite systems by redundant rules. In: Proceedings of 26th RTA. LIPIcs, vol. 36, pp. 257–268 (2015). doi:10.4230/LIPIcs.RTA.2015.257

23.

Nagele, J., Felgenhauer, B., Zankl, H.: Certifying confluence proofs via relative termination and rule labeling. LMCS (to appear) (2017)

24.

Nagele, J., Middeldorp, A.: Certification of classical confluence results for left-linear term rewrite systems. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 290–306. Springer, Cham (2016). doi:10.1007/978-3-319-43144-4_18 CrossRef

25.

Nagele, J., Thiemann, R.: Certification of confluence proofs using CeTA. In: Proceedings of 3rd IWC, pp. 19–23 (2014)

26.

Nelson, G., Oppen, D.: Fast decision procedures based on congruence closure. JACM 27(2), 356–364 (1980). doi:10.1145/322186.322198 MathSciNetCrossRefMATH

27.

Nipkow, T.: Higher-order critical pairs. In: Proceedings of 6th LICS, pp. 342–349 (1991). doi:10.1109/LICS.1991.151658

28.

Nipkow, T.: Functional unification of higher-order patterns. In: Proceedings of 8th LICS, pp. 64–74 (1993). doi:10.1109/LICS.1993.287599

29.

van Oostrom, V.: Developing developments. TCS 175(1), 159–181 (1997). doi:10.1016/S0304-3975(96)00173-9 MathSciNetCrossRefMATH

30.

van Oostrom, V., Raamsdonk, F.: Weak orthogonality implies confluence: the higher-order case. In: Nerode, A., Matiyasevich, Y.V. (eds.) LFCS 1994. LNCS, vol. 813, pp. 379–392. Springer, Heidelberg (1994). doi:10.1007/3-540-58140-5_35 CrossRef

31.

Oyamaguchi, M., Hirokawa, N.: Confluence and critical-pair-closing systems. In: Proceedings of 3rd IWC, pp. 29–33 (2014)

32.

Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. JACM 28(2), 233–264 (1981). doi:10.1145/322248.322251 MathSciNetCrossRefMATH

33.

van Raamsdonk, F.: On termination of higher-order rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 261–275. Springer, Heidelberg (2001). doi:10.1007/3-540-45127-7_20 CrossRef

34.

Regnier, L.: Une équivalence sur les lambda-termes. TCS 126(2), 281–292 (1994). doi:10.1016/0304-3975(94)90012-4 CrossRefMATH

35.

Rosen, B.: Tree-manipulating systems and Church-Rosser theorems. JACM 20(1), 160–187 (1973). doi:10.1145/321738.321750 MathSciNetCrossRefMATH

36.

Rubio, A.: A fully syntactic AC-RPO. I&C 178(2), 515–533 (2002). doi:10.1006/inco.2002.3158 MathSciNetMATH

37.

Sakai, M., Oyamaguchi, M., Ogawa, M.: Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 111–126. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_7 CrossRef

38.

Shintani, K., Hirokawa, N.: CoLL: A confluence tool for left-linear term rewrite systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 127–136. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_8 CrossRef

39.

Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: Proceedings of 24th RTA. LIPIcs, vol. 21, pp. 287–302 (2013).doi:10.4230/LIPIcs.RTA.2013.287

40.

Sternagel, C., Thiemann, R.: The certification problem format. In: Proceedings of 11th UITP. EPTCS, vol. 167, pp. 61–72 (2014). doi:10.4204/EPTCS.167.8

41.

Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452–468. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_31 CrossRef

42.

Toyama, Y.: Commutativity of term rewriting systems. In: Fuchi, K., Kott, L. (eds.) Programming of Future Generation Computers II, pp. 393–407. North-Holland Publishing, North Holland (1988)

43.

Toyama, Y., Oyamaguchi, M.: Church-Rosser property and unique normal form property of non-duplicating term rewriting systems. In: Proceedings of the 4th CTRS withDershowitz N., Lindenstrauss N. (eds.) CTRS 1994. LNCS, vol. 968 (1995). doi:10.1007/3-540-60381-6_19

44.

Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI – a confluence tool. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 499–505. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_38 CrossRef

45.

Zankl, H., Felgenhauer, B., Middeldorp, A.: Labelings for decreasing diagrams. JAR 54(2), 101–133 (2015). doi:10.1007/s10817-014-9316-y MathSciNetCrossRefMATH

Titel: CSI: New Evidence – A Progress Report
verfasst von: Julian Nagele
Bertram Felgenhauer
Aart Middeldorp
Verlag: Springer International Publishing
Buch: Automated Deduction – CADE 26
Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-63046-5_24

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"