Regular path expressions in feature logic (Q1333157)

The present paper is devoted to the investigation of the existential fragment of a feature logic, which is extended by regular path expressions. The language of this feature logic is based on a signature \(\sigma\) containing a set \(S\) of unitary predicate symbols \(A, B, \dots,\) and a set \(F\) of binary functional relational symbols, called features. There are two kinds of variables: first order variables \(x, y, \dots,\) and path variables \(p\), \(q\), \(r\), varying over the set \(F^ +\) of nonempty strings over \(F\). Atomic formulas have the form \(A(x)\), \(x = y\), \(xf_ 1 \dots f_ ny\), \(t \in L\), \(\div(u,v)\), \(u<v\), \(p = q\), \(t\), \(u\), \(v\) are strings of path variables. \(L\) is a regular expression denoting a regular sublanguage of \(F^ +\). A clause \(C\) is a conjunction of atomic formulas. In the paper is proved that the set \(\text{Sat}(\sigma)\) of all satisfiable clauses is decidable. This is shown by transforming a clause \(C\) into a finite set \(\text{Solv}(C)\) of so called solved clauses interpreted as a disjunction. Then it is proved that \(C\) is satisfiable if and only if \(\text{Solv}(C)\) is not empty. This interesting result is an extension of a result by Kaplan/Maxwell who proved the decidability of the pure existencial fragment, provided that a certain acyclicity condition is met.