nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Deciding the First-Order Theory of an Algebra of Feature Trees with Updates

verfasst von : Nicolas Jeannerod, Ralf Treinen

Erschienen in: Automated Reasoning

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

We investigate a logic of an algebra of trees including the update operation, which expresses that a tree is obtained from an input tree by replacing a particular direct subtree of the input tree, while leaving the rest unchanged. This operation improves on the expressivity of existing logics of tree algebras, in our case of feature trees. These allow for an unbounded number of children of a node in a tree.

We show that the first-order theory of this algebra is decidable via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers. This study is motivated by the logical modeling of transformations on UNIX file system trees expressed in a simple programming language.

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 Constructive Decision via Redundancy-Free Proof-Search

Nächstes Kapitel A Separation Logic with Data: Small Models and Automation

Aït-Kaci, H., Podelski, A., Smolka, G.: A feature-based constraint system for logic programming with entailment. Theor. Comput. Sci. 122(1–2), 263–283 (1994)CrossRef

Bach, M.: The Design of the UNIX Operating System. Prentice-Hall, Upper Saddle River (1986)

Backofen, R.: A complete axiomatization of a theory with feature and arity constraints. J. Log. Program. 24(1&2), 37–71 (1995)MathSciNetCrossRef

Backofen, R., Smolka, G.: A complete and recursive feature theory. Theor. Comput. Sci. 146(1–2), 243–268 (1995)MathSciNetCrossRef

Backofen, R., Treinen, R.: How to win a game with features. Inf. Comput. 142(1), 76–101 (1998)MathSciNetCrossRef

Comon, H., Lescanne, P.: Equational problems and disunification. J. Symb. Comput. 7, 371–425 (1989)MathSciNetCrossRef

Debian Policy Mailing List: Debian Policy Manual, Version 4.1.3. Debian, December 2017. https://www.debian.org/doc/debian-policy/

Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465–476 (1979)MathSciNetCrossRef

Hodges, W.: Model Theory, Encyclopedia of Mathematics and Its Applications, vol. 42. Cambridge University Press, Cambridge (1993)

10.

Jeannerod, N., Marché, C., Treinen, R.: A formally verified interpreter for a shell-like programming language. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 1–18. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72308-2_1CrossRef

11.

Jeannerod, N., Treinen, R.: Deciding the first-order theory of an algebra of feature trees with updates (extended version), January 2018. https://hal.archives-ouvertes.fr/hal-01760575

12.

Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: LICS, pp. 348–357. IEEE, Edinburgh, July 1988

13.

Malc’ev, A.I.: Axiomatizable classes of locally free algebras of various type (Chap. 23). In: Wells I, B.F. (ed.) The Metamathematics of Algebraic Systems: Collected Papers 1936–1967, pp. 262–281. North Holland, Amsterdam (1971)

14.

Smolka, G.: Feature constraint logics for unification grammars. J. Log. Program. 12, 51–87 (1992)MathSciNetCrossRef

15.

Smolka, G., Treinen, R.: Records for logic programming. J. Log. Program. 18(3), 229–258 (1994)MathSciNetCrossRef

16.

Treinen, R.: Feature constraints with first-class features. In: Borzyszkowski, A.M., Sokołowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 734–743. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57182-5_64CrossRef

17.

Treinen, R.: Feature trees over arbitrary structures (Chap. 7). In: Blackburn, P., de Rijke, M. (eds.) Specifying Syntactic Structures, pp. 185–211. CSLI Publications and FoLLI, Stanford (1997)

18.

Vorobyov, S.: An improved lower bound for the elementary theories of trees. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 275–287. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61511-3_91CrossRef

Titel: Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
verfasst von: Nicolas Jeannerod
Ralf Treinen
Verlag: Springer International Publishing
Buch: Automated Reasoning
Print ISBN: 978-3-319-94204-9

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

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94205-6_29

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"

Premium Partner