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

Simple counting quantifiers that can be used to compare the number of role successors of an individual or the cardinality of a concept with a fixed natural number have been employed in Description Logics (DLs) for more than two decades, under the respective names of number restrictions [8,13,12] and cardinality restrictions on concepts (CRs, CBoxes) [4,19]. The DL ALCQ [12] extends the basic DL ALC with so-called qualified number restrictions of the form (≥n r.C) and (≤n r.C), collecting individuals for which the number of r successors belonging to the concept C is bounded from below/above by the natural number n. The computational complexity of concept satisfiability in ALCQ [12] has been shown to be PSpace-complete without concept inclusions (CIs, TBoxes) and ExpTime-complete w.r.t. CIs, independently from the encoding (unary or binary) of the numbers occurring in the restrictions [18,20]. CRs are global constraints of the form (≥nC) and (≤nC), which state a lower/upper bound on how many elements of C a model may contain. By replacing CIs with CRs, the complexity of satisfiability increases to NExpTimecomplete if the numbers occurring in the CRs are assumed to be encoded in binary [19]. With unary coding of numbers, it stays ExpTime-complete even w.r.t. CRs [19]. It should be noted that both qualified number restrictions and CRs (which generalize CIs) can be expressed in C, the two-variable fragment of first-order logic with counting quantifiers [11,16], whose satisfiability problem is known to be NExpTime-complete [17]. Qualified number restrictions cannot relate cardinalities of different sets of role successors to one another, but can only compare the number of role successors (satisfying certain properties) of an individual against a fixed natural number. To overcome this limitation, in [1] we extended ALCQ by enabling the statement of restrictions on role successors using the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA) [14], in which one can express Boolean combinations of set constraints and numerical constraints comparing the cardinalities of finite sets. The resulting logic, called ALCSCC, strictly extends the expressive power of ALCQ. In [1] it is shown that the ALCSCC concept description succ(|r| = |s|), which describes individuals having the same number of r-successors as s-successors, cannot be expressed in ALCQ. In addition, it has been shown in [5] that succ(|r∩A| = |r∩¬A|), the ALCSCC concept

Description Logics That Count, and What They Can and Cannot Count