English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Matching is the special case of unification where one of the expressions to be unified has no variables and thus remains unchanged under substitutions. In Description Logic (DL), matching of concept descriptions against concept patterns was originally introduced in [12] as a non-standard inference task that can be used to filter out the unimportant aspects of large concept descriptions appearing in knowledge bases of the system Classic [10]. Subsequently, matching (as well as the more general problem of unification) was also proposed as a tool for detecting redundancies in knowledge bases [9] and to support the integration of knowledge bases by prompting interschema assertions to the integrator [11]. All three applications have in common that one wants to search the knowledge base for concepts having a certain (not completely specified) form. This “form” can be expressed with the help of so-called concept patterns, i.e., concept descriptions containing variables (which stand for concept descriptions). For example, assume that we want to find concepts that are concerned with humans that share some characteristic with all their children. This can be expressed by the pattern D := Human u X u ∀has-child.X where X is a variable standing for the common characteristic. The concept description C := HumanuTallu∀has-child.Tall matches this pattern in the sense that, if we replace the variable X by the concept description Tall, the pattern becomes equivalent to the concept description C. Thus, the substitution σ := {X 7→ Tall} is a matcher of the matching problem C ≡ D since C ≡ σ(D). Both matching and unification have been investigated in detail for the inexpressive DLs FL0 (with concept constructors top >, conjunction C uD, value restriction ∀r.C) and EL (with concept constructors >, CuD, existential restriction ∃r.C). Whereas in EL both matching [6] and unification [7] are NP-complete problems, the complexity of these problems differs significantly for FL0: matching is polynomial, but unification is ExpTime-complete [9]. These results were shown for the case without a background TBox, i.e., a finite set of general concept inclusions (GCIs). For the DL EL it was proved in [8] that the presence of TBoxes does not change the complexity of the matching problem: it stays in NP. For unification in EL w.r.t. TBoxes, an NP upper bound could until now only be shown for a restricted form of TBoxes [2].

Matching in the Description Logic FL0 with respect to General TBoxes