Regular path expressions in feature logic (Q1333157)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Regular path expressions in feature logic
scientific article

    Statements

    Regular path expressions in feature logic (English)
    0 references
    0 references
    13 September 1994
    0 references
    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.
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    knowledge representation
    0 references
    feature descriptions
    0 references
    decidability
    0 references
    feature logic
    0 references
    acyclicity
    0 references
    0 references