Research Internship of level Master-2:
A logical theory of trees with updates

Feature Trees have been used in various areas of computer science like artificial intelligence, computational linguistics, knowledge representation [Kel93], and also as a general model of data for logic programming languages [ST94]. These trees, and their pertaining description languages, allow for descriptions of trees that are finer grained than standard term languages, and that are designed for situations in which one has to deal with incomplete information about trees. One distinguishing treat of feature trees and their description languages is that they allow to denote a specific subtree of a tree via an access path from the root of tree.

Many problems related to the analysis of feature tree descriptions can be expressed in terms of first-order formulas. There has been a number of works investigating decidability questions of various first-order theories of feature trees, like the works on decidability of the first-order theories FT [BS95], CFT [Bac95], or a generalization which is parameterized by a theory of edge labelings [Tre97]. A further generalization that models edge labelings as first-class values has an undecidable first-order theory [Tre93].

All these works have been concerned with first-order logics of description languages of feature trees, that is their focus was on static aspects of feature trees. The topic of the work we propose here is to investigate algorithmic properties of a theory of feature trees with updates. Updates are local modifications of feature trees, they allow to modify a subtree of a given tree at a given address. The purpose of a theory of feature trees with updates would be to describe the semantics of complex modifications of a tree. Our main application here consists in feature trees as an abstraction of the state of a UNIX-like file system, and to use a logics of feature trees in order to formalize the effect of a process that manipulates a file system (for instance a shell script using UNIX commands like mkdir, ln, rm, …). The question is whether the first-order theory of feature trees with updates is decidable.

The long-term goal of this line of research, and a possible subject of a PhD thesis, is to develop methods and automatic tools for the specification and verification of programs that manipulate persistent and complex hierarchical data, like a UNIX file systems. A decision algorithm for the first-order theory of feature trees with updates would constitute only a first step in this direction.

Prerequisites

Methods for deciding first-order theories (in particular quantifier elimination), as taught in the module démonstration automatique of MPRI.

Supervisor

Ralf Treinen

Venue

References

[Bac95]

Rolf Backofen. A complete axiomatization of a theory with feature and arity constraints. Journal of Logic Programming, 24(1&2):37–71, July/August 1995.

[BS95]

Rolf Backofen and Gert Smolka. A complete and recursive feature theory. Theoretical Computer Science, 146(1–2):243–268, July 1995.

[Kel93]

Bill Keller. Feature Logics, Infinitary Descriptions and Grammar. CSLI Lecture Notes No. 44. Center for the Study of Language and Information, 1993.

[ST94]

Gert Smolka and Ralf Treinen. Records for logic programming. Journal of Logic Programming, 18(3):229–258, April 1994.

[Tre93]

Ralf Treinen. Feature constraints with first-class features. In Andrzej M. Borzyszkowski and Stefan Sokołowski, editors, Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, pages 734–743. Springer-Verlag, August/September 1993.

[Tre97]

Ralf Treinen. Feature trees over arbitrary structures. In Patrick Blackburn and Maarten de Rijke, editors, Specifying Syntactic Structures, chapter 7, pages 185–211. CSLI Publications and FoLLI, 1997.

This document was translated from L^AT_EX by H^EV^EA.