Search

We study the problem of none-stable truth values for modal formulas. Our aim is to investigate temporal-modal logics for description reliability of information. We investigate a logic with rather standard relational models for branching time logic. But we study an unusual task – intervals of none-stable truth values of formulas. None-stable truth values for formulas means that formulas for a long time change their truth values from true to false and vice versa. We found an algorithm which may recognize permanently none-stable formulas. [ABSTRACT FROM AUTHOR]

We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical section are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invariants allowing the proof of general safety properties. The invariants are defined using the WS κ S fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection, thus reducing a verification problem to checking satisfiability of a WS κ S formula. • We introduce a logic-based language for describing sets of configurations of parameterized distributed systems. • The language uses predicate symbols to hierarchically decompose the system architecture into specific patterns. • We address a parametric safety problem i.e., checking that reachable configurations stay clear of error configurations. • We show that deadlock freedom and critical section violation problems are undecidable, even for simple architectures. • We develop a verification method that synthesizes parametric invariants described using a decidable fragment of MSO. [ABSTRACT FROM AUTHOR]

We present DEGARI 2.0 (Dynamic Emotion Generator And ReclassIfier): an explainable, affective-based, art recommender relying on the commonsense reasoning framework T CL and exploiting an ontological model formalizing the Plutchik's theory of emotions. The main novelty of this system relies on the development of diversity-seeking affective recommendations obtained by exploiting the spatial structure of the Plutchik's 'wheel of emotion'. In particular, such development allows to classify and to suggest, to museum users, cultural items able to evoke not only the very same emotions of already experienced or preferred objects (e.g. within a museum exhibition), but also novel items sharing different emotional stances. The system's goal, therefore, is to break the filter bubble effect and open the users' view towards more inclusive and empathy-based interpretations of cultural content. The system has been tested, in the context of the EU H2020 SPICE project, on the community of deaf people and on the collection of the GAM Museum of Turin. We report the results and the lessons learnt concerning both the acceptability and the perceived explainability of the received diversity-seeking recommendations. [ABSTRACT FROM AUTHOR]

The aim of the present paper is to prove that concept validity and positive satisfiability with an empty ontology in the Fuzzy Description Logic I ALE , under standard product semantics and with respect to quasi-witnessed models, are decidable. In our framework we are not considering reasoning tasks over ontologies. The proof of our result consists in reducing the problem to a finitary consequence problem in propositional product logic with Monteiro-Baaz delta operator, which is known to be decidable. Product FDL and first order logic are known not to enjoy the finite model property, so we cannot restrict to finite interpretations. Thus, in order to obtain our result, we need to codify infinite interpretations using a finite number of propositional formulas. Such result was conjectured in [10] , but the proof given was subsequently found incorrect. In the present work an improved reduction algorithm is proposed and a proof of the same result is provided. [ABSTRACT FROM AUTHOR]

Controlled Query Evaluation (CQE) is a framework for the protection of confidential data, where a policy given in terms of logic formulae indicates which information must be kept private. Functions called censors filter query answering so that no answers are returned that may lead a user to infer data protected by the policy. The preferred censors, called optimal censors, are the ones that conceal only what is necessary, thus maximizing the returned answers. Typically, given a policy over a data or knowledge base, several optimal censors exist. Our research on CQE is based on the following intuition: confidential data are those that violate the logical assertions specifying the policy, and thus censoring them in query answering is similar to processing queries in the presence of inconsistent data as studied in Consistent Query Answering (CQA). In this paper, we investigate the relationship between CQE and CQA in the context of Description Logic ontologies. We borrow the idea from CQA that query answering is a form of skeptical reasoning that takes into account all possible optimal censors. This approach leads to a revised notion of CQE, which allows us to avoid making an arbitrary choice on the censor to be selected, as done by previous research on the topic. We then study the data complexity of query answering in our CQE framework, for conjunctive queries issued over ontologies specified in the popular Description Logics DL-Lite R and EL ⊥. In our analysis, we consider some variants of the censor language, which is the language used by the censor to enforce the policy. Whereas the problem is in general intractable for simple censor languages, we show that for DL-Lite R ontologies it is first-order rewritable, and thus in AC0 in data complexity, for the most expressive censor language we propose. [ABSTRACT FROM AUTHOR]

There are two kinds of bisimulation, namely crisp and fuzzy , between fuzzy structures such as fuzzy automata, fuzzy labeled transition systems, fuzzy Kripke models and fuzzy interpretations in description logics. Fuzzy bisimulations between fuzzy automata over a complete residuated lattice have been introduced by Ćirić et al. in 2012. Logical characterizations of fuzzy bisimulations between fuzzy Kripke models (respectively, fuzzy interpretations in description logics) over the residuated lattice [ 0 , 1 ] with the Gödel t-norm have been provided by Fan in 2015 (respectively, Nguyen et al. in 2020). There was the lack of logical characterizations of fuzzy bisimulations between fuzzy graph-based structures over a general residuated lattice, as well as over the residuated lattice [ 0 , 1 ] with the Łukasiewicz or product t-norm. In this article, we provide and prove logical characterizations of fuzzy bisimulations in fuzzy modal logics over residuated lattices. The considered logics are the fuzzy propositional dynamic logic and its fragments. Our logical characterizations concern invariance of formulas under fuzzy bisimulations and the Hennessy-Milner property of fuzzy bisimulations. They can be reformulated for other fuzzy structures such as fuzzy labeled transition systems and fuzzy interpretations in description logics. [ABSTRACT FROM AUTHOR]

This article explores how the academic field of gender and feminist studies in England represents itself, by drawing on a discourse analysis of online descriptions from websites of all gender and feminist studies degree programmes and departments in English universities, all but one of which are graduate degrees. Foregrounding the context of the neoliberal university, in which feminist and gender knowledge is simultaneously marginalised and mainstreamed, the article asks how representations of the field are shaped by the marketisation of higher education. This analysis reveals a disjuncture between two representative logics: while most feminist, gender studies and queer scholarship relies on anti-essentialist epistemologies and ontologies, the dominant logic of representation in contemporary universities understands difference as static and representable. This representability enables and is in turn facilitated by marketisation. [ABSTRACT FROM AUTHOR]

The Ontology-Based Data Access (OBDA) systems allows users to access external databases through a conceptual domain view, given in terms of an ontology. This semantic technology addresses such problems as conceptual modeling, query rewriting, an source-to-target mapping. We show how these issues have been defined and implemented in the DAFO system, highlighting those features that distinguish it from the standard OBDA system. We propose an original approach to cope with the trade-off between expressiveness of the ontology-based conceptual modelling and ontology-mediated query rewriting in the DAFO systems. For this purpose, we divide ontological rules into three parts: (a) rewriting rules, (b) rules defining intensional predicates (views), and (c) constraint rules (satisfied in the database). This allows to balance the semantic power of the conceptual modeling and the effciency of query answering in the DAFO system, where queries are based on the faceted query paradigm. [ABSTRACT FROM AUTHOR]

Depuis le début du XXe siècle la question du double hante les psychopathologues de divers horizons. Pourtant même les travaux contemporains laissent toujours une zone d'ombre concernant la fonction subjective du dédoublement. Dans le présent travail il s'agira d'examiner ce phénomène pour en proposer une interprétation conceptuelle. Nous allons reprendre un exemple clinique devenu classique dans la phénoménologie du dédoublement, le cas de la vie et de l'œuvre de Maupassant, pour le mettre à l'épreuve du concept de temporalité structurale de la subjectivation psychotique de la jouissance telle qu'elle peut être conceptualisée par la psychanalyse contemporaine. Pour approcher le tableau du dédoublement dans cette perspective, il nous faut dépasser le regard fasciné par la coupe synchronique du phénomène pour l'inscrire dans la diachronie d'une logique temporelle de la psychose susceptible d'expliquer ses étapes. L'élaboration nous introduira à une clinique différentielle des diverses modalités temporelles de la subjectivation délirante du double qui enrichit la compréhension de la dynamique subjective de l'œuvre littéraire et sa fonction dans l'expérience psychotique. En reprenant au fil de notre réflexion les références psychiatriques et psychanalytiques concernant la question du double nous démontrons la pertinence de l'abord structural du problème. La subjectivation du double, loin de se réduire à une simple manifestation d'un trouble, exprime, au moins dans certains cas, une tentative d'auto-agencement subjectif de la psychose qui permet au sujet d'éviter la déstructuration dissociative. Since the beginning of the twentieth century, the question of the double has haunted psychopathologists of various horizons. However, even contemporary works always leave a shadow area concerning the subjective function of the double. In this work, we will examine this phenomenon in order to propose a conceptual interpretation of it. We will take up a clinical example that has become a classic in the phenomenology of the double, the case of Maupassant's life and work, and put it to the test of the concept of the structural temporality of the psychotic subjectivation of jouissance as conceptualized by contemporary psychoanalysis. Understanding the phenomenon of the double in this perspective requires us to go beyond the fascination with the synchronic rupture inherent in this phenomenon; instead, we must include it in the diachrony of a temporal logic of psychosis that is able to explain its stages. This elaboration will introduce us to a differential clinic of the various temporal modalities of the delusional subjectivation of the double, which helps us to better understand the subjective dynamic of the literary work and its function in the psychotic experience. By including psychiatric and psychoanalytic references in our reflections on the questions of the double, we demonstrate the relevance of the structural approach to the problem. The subjectivation of the double, far from being reduced to a simple manifestation of a disorder, expresses, at least in some cases of psychosis, an attempt at subjective self-organization that allows the subject to avoid dissociative destructuring. [ABSTRACT FROM AUTHOR]

Description logics (DLs) are a suitable formalism for representing knowledge about domains in which objects are described not only by attributes but also by binary relations between objects. Fuzzy extensions of DLs can be used for such domains when data and knowledge about them are vague and imprecise. One of the possible ways to specify classes of objects in such domains is to use concepts in fuzzy DLs. As DLs are variants of modal logics, indiscernibility in DLs is characterized by bisimilarity. The bisimilarity relation of an interpretation is the largest auto-bisimulation of that interpretation. In DLs and their fuzzy extensions, such equivalence relations can be used for concept learning. In this paper, we define and study fuzzy bisimulation and bisimilarity for fuzzy DLs under the Gödel semantics, as well as crisp bisimulation and strong bisimilarity for such logics extended with involutive negation. The considered logics are fuzzy extensions of the DL ALC r e g (a variant of PDL) with additional features among inverse roles, nominals, (qualified or unqualified) number restrictions, the universal role, local reflexivity of a role and involutive negation. We formulate and prove results on invariance of concepts under fuzzy (resp. crisp) bisimulation, conditional invariance of fuzzy TBoxes/ABoxes under bisimilarity (resp. strong bisimilarity), and the Hennessy-Milner property of fuzzy (resp. crisp) bisimulation for fuzzy DLs without (resp. with) involutive negation under the Gödel semantics. Apart from these fundamental results, we also provide results on using fuzzy bisimulation to separate the expressive powers of fuzzy DLs, as well as results on using strong bisimilarity to minimize fuzzy interpretations. [ABSTRACT FROM AUTHOR]

Ontology learning techniques are based on extensive basic knowledge, from unstructured data to structured data. Creating an ontology manually is undoubtedly a time consuming process. In addition, manually-curated background knowledge is a scarce resource for many domains. Ontology learning is a relatively new research area that draws from related fields. However, a number of approaches are still rising up and, what is more, they vary and evolve across different aspects. Therefore, the purpose of this article is to provide comprehensive knowledge about selected groups of methods, tools and approaches supporting ontology. Presenting different approaches to learning ontology and including them in one publicly available summary, aims to provide an overview of the most appropriate methods, tools and approaches to building ontologies from various sources. Besides, the proposed solution in this article will expand the already offered ontology of learning methods with additional, more detailed functions. In addition to the domain ontology offered, this is another goal of this article. The correctness of the proposed ontology was verified by the constructed competence questions and implemented using Description Logic query mechanism. [ABSTRACT FROM AUTHOR]

In the paper we present the results of experiment we performed to determine whether a contextual approach may be used to increase the performance of querying a knowledge base. For the experiments we have used a unique setting where we put much effort in developing a contextual and a non-contextual ontology which are as much close counterparts as possible. To achieve this we created a contextual version of a non-contextual ontology and reformulated the set of competency questions to reflect the contextual structure of the newly created knowledge base. The results of the experiment strongly suggest that using contexts might be advantageous for improving performance, and also show the further ways of development of the approach. [ABSTRACT FROM AUTHOR]

The rapid development of the Internet of Things (IoT) and the huge growth of valuable data produced by decentralising information processing along global apparel supply chain have led to a persuasive appeal for a semantic approach to integrating distributed data facilities in the field of self-determining collaborating logistics services. This paper describes a framework, Apparel Business Decentralised Data Integration (ABDDI), which exploits knowledge representation techniques and languages (e.g. Description Logics – DLs) to annotate relevant business activities, movements of products within the manufacturing network to provide value-added services. More specifically the paper discusses the DLs formalisms, which are used for knowledge representation in a decidable fragment of First Order Logic; and ALN (D) (Attributive Language with unqualified Number restrictions and concrete Domains) related issues. The paper presents an algorithm to demonstrate the DLs based entity concept similarity assessment to facilitate semantic web service. Finally, a business scenario is used to present some of the knowledge representation formalisms and concept similarity assessment in ABDDI. [ABSTRACT FROM AUTHOR]

We explore the relationships between Description Logics and Set Theory. The study is carried on using, on the set-theoretic side, a very rudimentary axiomatic set theory Ω, consisting of only four axioms characterizing binary union, set difference, inclusion, and the power-set. An extension of ALC , dubbed ALC Ω , is defined in which concepts are naturally interpreted as sets living in Ω-models. In ALC Ω not only membership between concepts is allowed—even admitting membership circularity—but also the power-set construct is exploited to add metamodelling capabilities. We investigate translations of ALC Ω into standard description logics as well as a set-theoretic translation. A polynomial encoding of ALC Ω in ALCOI proves the validity of the finite model property as well as an ExpTime upper bound on the complexity of concept satisfiability. We develop a set-theoretic translation of ALC Ω in the theory Ω, exploiting a technique proposed for translating normal modal and polymodal logics into Ω. Finally, we show that the fragment LC Ω of ALC Ω not admitting roles and individual names, is as expressive as ALC Ω. [ABSTRACT FROM AUTHOR]

We study the relative expressiveness of ontology-mediated queries (OMQs) formulated in the expressive Description Logic ALCHOIQ extended with closed predicates. In particular, we present a polynomial time translation from OMQs into Datalog with negation under the stable model semantics, the formalism that underlies Answer Set Programming. This is a novel and non-trivial result: the considered OMQs are not only non-monotonic, but also feature a tricky combination of nominals, inverse roles, and counting. We start with atomic queries and then lift our approach to a large class of first-order queries where quantification is "guarded" by closed predicates. Our translation is based on a characterization of the query answering problem via integer programming, and a specially crafted program in Datalog with negation that finds solutions to dynamically generated systems of integer inequalities. As an important by-product of our translation we get that the query answering problem is co-NP-complete in data complexity for the considered class of OMQs. Thus, answering these OMQs in the presence of closed predicates is not harder than answering them in the standard setting. This is not obvious as closed predicates are known to increase data complexity for some existing ontology languages. [ABSTRACT FROM AUTHOR]

The problem of minimizing finite fuzzy interpretations in fuzzy description logics (FDLs) is worth studying. For example, the structure of a fuzzy/weighted social network can be treated as a fuzzy interpretation in FDLs, where actors are individuals and actions are roles. Minimizing the structure of a fuzzy/weighted social network makes it more compact, thus making network analysis tasks more efficient. In this work, we study the problem of minimizing a finite fuzzy interpretation in a FDL by using the largest crisp auto-bisimulation. The considered FDLs use the Baaz projection operator and their semantics is specified using an abstract algebra of fuzzy truth values, which can be any linear and complete residuated lattice. We provide an efficient algorithm with a complexity of O ((m log ⁡ l + n) log ⁡ n) for minimizing a given finite fuzzy interpretation I , where n is the size of the domain of I , m is number of nonzero instances of atomic roles of I and l is the number of different fuzzy values used for instances of atomic roles of I. We prove that the fuzzy interpretation returned by the algorithm is minimal among the ones that preserve fuzzy TBoxes and ABoxes under certain conditions. [ABSTRACT FROM AUTHOR]

• Proposing an iterative and incremental knowledge management model for problem solving. • Developing a new search intent predicting method. • Designing a knowledge learning strategy addressing knowledge visualization techniques. • Achieving an interactive healthcare knowledge management system. Healthcare is a knowledge intensive process, which requires large amount of information from various healthcare knowledge providers. However, this growing information makes challengeable for users in finding useful healthcare information to support their healthcare decision making. Knowledge management and knowledge management systems are drawing increasing attention in healthcare community. This paper proposes an online healthcare knowledge management framework and system prototype, featured with integrating knowledge learning and exploratory search for solving problems efficiently. Inspired by the knowledge to action framework in healthcare and the iterative process in software engineering, an iterative and incremental knowledge management model is designed to organize the activities during the knowledge learning and searching procedure. Supported by the knowledge-enhanced infrastructure of online healthcare information designed, domain knowledge learning and task knowledge learning environment can work collaboratively and interactively to improve the result of learning and exploratory search. Knowledge base also provides helpful information in an interactive way for solving problems. Given exploiting probabilistic information retrieval model and concept semantics described in Description Logics, a search intent discovery method and search intent guided learning and searching mechanism are designed within this environment for achieving the learning and search goal. The results of the experiments have proved the efficacy of the methods and process model used in the leaning-focused healthcare knowledge management system. [ABSTRACT FROM AUTHOR]

The notion of a most specific consequence with respect to some terminological box is introduced, conditions for its existence in the description logic E L and its variants are provided, and means for its computation are developed. Algebraic properties of most specific consequences are explored. Furthermore, several applications that make use of this new notion are proposed and, in particular, it is shown how given terminological knowledge can be incorporated in existing approaches for the axiomatization of observations. For instance, a procedure for an incremental learning of concept inclusions from sequences of interpretations is developed. [ABSTRACT FROM AUTHOR]

Ontology-based data access (OBDA) is a popular approach for integrating and querying multiple data sources by means of a shared ontology. The ontology is linked to the sources using mappings, which assign to ontology predicates views over the data. The conventional semantics of OBDA is set-based—that is, the extension of the views defined by the mappings does not contain duplicate tuples. This treatment is, however, in disagreement with the standard semantics of database views and database management systems in general, which is based on bags and where duplicate tuples are retained by default. The distinction between set and bag semantics in databases is very significant in practice, and it influences the evaluation of aggregate queries. In this article, we propose and study a bag semantics for OBDA which provides a solid foundation for the future study of aggregate and analytic queries. Our semantics is compatible with both the bag semantics of database views and the set-based conventional semantics of OBDA. Furthermore, it is compatible with existing bag-based semantics for data exchange recently proposed in the literature. We show that adopting a bag semantics makes conjunctive query answering in OBDA coNP -hard in data complexity. To regain tractability of query answering, we consider suitable restrictions along three dimensions, namely, the query language, the ontology language, and the adoption of the unique name assumption. Our investigation shows a complete picture of the computational properties of query answering under bag semantics over ontologies in the DL-Lite family. [ABSTRACT FROM AUTHOR]

Rational closure is one of the most extensively studied nonmonotonic extensions of description logics. Nonetheless, so far it has been investigated only for description logics that satisfy the disjoint model union property, or limited fragments that support nominals. In this paper we show that for sufficiently expressive description logics, the traditional correspondence between rational closure and ranked interpretations does not hold. Therefore, in order to extend rational closure to a wider class of description logics it is necessary to change the definition of rational closure, or alternatively abandon its standard semantics. Here we pursue the former approach, and introduce stable rational closure , based on stable rankings. The resulting nonmonotonic logic is a natural extension of the standard rational closure: First, its refined exceptionality criterion yields a closure that satisfies the KLM postulates. Second, when a knowledge base enjoys the disjoint model union property, then stable rational closure equals the old notion. In the other cases, stable rankings may raise the exceptionality level of some concepts. Stable rational closure has a model-theoretic semantics based on upward-closed models, that relax the canonical models adopted in the past, in order to deal with logics that do not satisfy the disjoint union model property. Unfortunately, stable rankings do not always exist, and are not necessarily unique. However, they can be effectively enumerated for all defeasible knowledge bases in SROIQ , using any algorithm for reasoning with ranked models. [ABSTRACT FROM AUTHOR]

Domain ontologies are pivotal for Semantic Web applications. The richness of an ontology goes in hand with its usefulness and efficiency. Unfortunately, manually enriching an ontology is very time-consuming. In this paper, we propose to enrich an ontology automatically by obtaining logical expressions of concepts. We present NALDO, a novel approach that provides an OWL DL (Web Ontology Language Description Logics) expression of a concept from two inputs: (1) the natural language definition of the concept and (2) an ontology describing the domain of this concept. NALDO uses as much as possible entities provided by the domain ontology, however it can suggest, when needed, new entities. The expressiveness of expressions provided by NALDO covers value and cardinality restrictions, subsumption and equivalence. We evaluate our approach against the definitions and the corresponding ontologies of the BEAUFORD benchmark. Our results show that NALDO is able to perform the correct identification of formal entities with an F1-measure up to 0.79. [ABSTRACT FROM AUTHOR]

We investigate the problem whether two ALC ontologies are indistinguishable (or inseparable) by means of queries in a given signature, which is fundamental for ontology engineering tasks such as ontology versioning, modularisation, update, and forgetting. We consider both knowledge base (KB) and TBox inseparability. For KBs, we give model-theoretic criteria in terms of (finite partial) homomorphisms and products and prove that this problem is undecidable for conjunctive queries (CQs), but 2 ExpTime -complete for unions of CQs (UCQs). The same results hold if (U)CQs are replaced by rooted (U)CQs, where every variable is connected to an answer variable. We also show that inseparability by CQs is still undecidable if one KB is given in the lightweight DL EL and if no restrictions are imposed on the signature of the CQs. We also consider the problem whether two ALC TBoxes give the same answers to any query over any ABox in a given signature and show that, for CQs, this problem is undecidable, too. We then develop model-theoretic criteria for Horn ALC TBoxes and show using tree automata that, in contrast, inseparability becomes decidable and 2 ExpTime -complete, even ExpTime -complete when restricted to (unions of) rooted CQs. [ABSTRACT FROM AUTHOR]

Metadata and ontologies are used to enable computers to read data on the Semantic Web. Description logics provide formal languages and reasoning algorithms for such metadata and ontologies. Tableau-based algorithms have been developed for deciding concept satisfiability in description logics but they lead to inefficient reasoning for complex logical expressions. The resolution principle and the Davis–Putnam–Logemann–Loveland (DPLL) solve the weakness by treating simplified clausal forms in description logics. However, resolution-based reasoning for description logics causes to compute various combinations of clause pairs to branch on. On the other hand, DPLL-based approaches have not presented a complete and decidable reasoning algorithm for directly deciding the satisfiability of clauses in description logics. In this paper, we propose a decidable and complete reasoning algorithm for clauses in description logic ALC. Using DPLL techniques, this algorithm can reduce reasoning steps for conjunctive normal form (CNF) concepts in ALC. We prove the termination, soundness, and completeness of the reasoning algorithm for the satisfiability of CNF concepts by introducing a restricted tableau for CNF concepts. We show some examples of reasoning steps for applying clauses in ALC to the algorithm. [ABSTRACT FROM AUTHOR]

In applications of AI systems where exact definitions of the important notions of the application domain are hard to come by, the use of traditional logic-based knowledge representation languages such as Description Logics may lead to very large and unintuitive definitions, and high complexity of reasoning. To overcome this problem, we define new concept constructors that allow us to define concepts in an approximate way. To be more precise, we present a family τ EL (m) of extensions of the lightweight Description Logic EL that use threshold constructors for this purpose. To define the semantics of these constructors we employ graded membership functions m , which for each individual in an interpretation and concept yield a number in the interval [ 0 , 1 ] expressing the degree to which the individual belongs to the concept in the interpretation. Threshold concepts C ⋈ t for ⋈ ∈ { < , ≤ , > , ≥ } then collect all the individuals that belong to C with degree ⋈ t. The logic τ EL (m) extends EL with threshold concepts whose semantics is defined relative to a function m. To construct appropriate graded membership functions, we show how concept measures ∼ (which are graded generalizations of subsumption or equivalence between concepts) can be used to define graded membership functions m ∼. Then we introduce a large class of concept measures, called simi-d , for which the logics τ EL (m ∼) have good algorithmic properties. Basically, we show that reasoning in τ EL (m ∼) is NP/coNP-complete without TBox, PSpace-complete w.r.t. acyclic TBoxes, and ExpTime-complete w.r.t. general TBoxes. The exception is the instance problem, which is already PSpace-complete without TBox w.r.t. combined complexity. While the upper bounds hold for all elements of simi-d , we could prove some of the hardness results only for a subclass of simi-d. This article considerably improves on and generalizes results we have shown in three previous conference papers and it provides detailed proofs of all our results. [ABSTRACT FROM AUTHOR]

Abstract The fuzzy UML model has been introduced to enable the conceptual modeling of imprecise data in many applications. How to prevent, detect, and correct errors as early as possible in the modeling process by verifying the correctness of fuzzy UML models is desirable. But it is difficult to manually verify the correctness of the models. Thanks to the effective reasoning service of fuzzy Description Logics (DLs), they are considered as natural candidates for supporting the verification of fuzzy UML models. In this paper we propose a complete and practical approach for verifying fuzzy UML models with fuzzy DLs. In detail, we first propose an approach for transforming a fuzzy UML model into a fuzzy DL knowledge base. Then we further reduce the verification tasks of the fuzzy UML model to reasoning problems of the transformed fuzzy DL knowledge base. Also, the correctness of the approach is proved, and a running example is provided to explain the approach in detail. Final we implemented a prototype that can transform fuzzy UML models into fuzzy DL knowledge bases. Case studies show that the proposed approach is feasible and the prototype translator actually works. By means of our approach and tool, the transformed fuzzy DL knowledge base and reasoning tasks can be input into the existing fuzzy DL reasoners, and the reasoning results reported by the reasoners can be passed back to the designer to improve the quality of the fuzzy UML model. Graphical abstract Highlights • Proposing an approach to transform a fuzzy UML model into a fuzzy DL knowledge base. • Proposing an approach to reduce verification tasks from fuzzy UML to fuzzy DL. • Implementing a prototype transformation tool. • Giving formal proofs, running example , and case studies. • Improving the quality of the fuzzy UML models. [ABSTRACT FROM AUTHOR]

Abstract Description Logics (DLs) are logics with interesting representational and computational features and are at the core of the Web Ontology Language OWL 2 and its profiles among which there is OWL 2 EL. The main feature of OWL 2 EL is that instance/subsumption checking can be decided in polynomial time. On the other hand, fuzzy DLs have been proposed as an extension to classical DLs with the aim of dealing with fuzzy concepts and we focus here on Fuzzy OWL 2 EL under standard and Gödel semantics. We provide some reasoning algorithms showing that instance/subsumption checking decision problems remain polynomial time for Fuzzy OWL 2 EL. We also identify some issues in previous related work (essentially incompleteness problems). [ABSTRACT FROM AUTHOR]

We report on a case study in which Password Authentication Connection Establishment (PACE) protocol has been formally analyzed based on its rewrite theory specification with Maude, a rewriting logic-based computer language and system. Dominik Klein has formally verified with interactive theorem proving that PACE enjoys the key secrecy property under the condition that the password shared by a passport chip C and a terminal T would be never leaked to the third party. In contrast, our analysis supposes that the password is leaked to an intruder once it has been used in a session completed. Under the condition, the analysis unveils some security weakness that PACE does not enjoy the correspondence (or authentication or agreement) properties from both C and T points of view. Then, we propose that one-time password is used in PACE. We have formally analyzed that the revised version enjoys the correspondence properties under the latter condition. We have used the Maude search command that can be used to conduct reachability analysis because the correspondence properties can be formalized as invariant properties. [ABSTRACT FROM AUTHOR]

We show that a Navigational Logic, i.e., a logic to express properties about graphs and about paths in graphs is a semi-exact institution. In this way, we can use a number of operations to structure and modularize our specifications. Moreover, using the properties of our institution, we also show how to structure single formulas, which in our formalism could be quite complex. [ABSTRACT FROM AUTHOR]

Self-adaptivity enables flexible solutions in dynamically changing environments. However, due to the increasing complexity, uncertainty, and topology changes in cyber-physical systems (CPS), static adaptation mechanisms are insufficient as they do not always achieve appropriate effects. Furthermore, CPS are used in safety-critical domains, which requires them and their autonomous adaptations to be dependable. To overcome these problems, we extend the MAPE-K feedback loop architecture by imposing a structure and requirements on the knowledge base and by introducing a meta-adaptation layer. This enables us to continuously evaluate the accuracy of previous adaptations, learn new adaptation rules based on executable run-time models, and verify the correctness of the adaptation logic in the current system context. We demonstrate the effectiveness of our approach using a temperature control system. With our framework, we enable the design of comprehensible and dependable dynamically evolving adaptation logics. [ABSTRACT FROM AUTHOR]

Space, as we typically represent it in mathematics and physics, is composed of dimensionless, indivisible points. On an alternative, region-based approach to space, extended regions together with the relations of ‘parthood’ and ‘contact’ are taken as primitive; points are represented as mathematical abstractions from regions. Region-based theories of space have been traditionally modeled in regular closed (or regular open) algebras, in work that goes back to [5] and [21] . Recently, logics for region-based theories of space were developed in [3] and [19] . It was shown that these logics have both a nice topological and relational semantics, and that the minimal logic for contact algebras, L m i n c o n t (defined below), is complete for both. The present paper explores the question of completeness of L m i n c o n t and its extensions for individual topological spaces of interest: the real line, Cantor space, the rationals, and the infinite binary tree. A second aim is to study a different, algebraic model of logics for region-based theories of space, based on the Lebesgue measure algebra (or algebra of Borel subsets of the real line modulo sets of Lebesgue measure zero). As a model for point-free space, the algebra was first discussed in [2] . The main results of the paper are that L m i n c o n t is weakly complete for any zero-dimensional, dense-in-itself metric space (including, e.g. , Cantor space and the rationals); the extension L m i n c o n t + ( C o n ) is weakly complete for the real line and the Lebesgue measure contact algebra. We also prove that the logic L m i n c o n t + ( U n i v ) is weakly complete for the infinite binary tree. [ABSTRACT FROM AUTHOR]

Dealing with context dependent knowledge is a well-known area of study that roots in John McCarthy's seminal work. More recently, the Contextualized Knowledge Repository (CKR) framework has been conceived as a logic-based approach in which knowledge bases have a two layered structure, modeled by a global context and a set of local contexts. The global context not only contains the meta-knowledge defining the properties of local contexts, but also holds the global (context independent) object knowledge that is shared by all of the local contexts. In many practical cases, however, it is desirable to leave the possibility to “override” the global object knowledge at the local level: in other words, it is interesting to recognize the pieces of knowledge that can admit exceptional instances in the local contexts that do not need to satisfy the general axiom. To address this need, we present in this paper an extension of CKR in which defeasible axioms can be included in the global context. The latter are verified in the local contexts only for the instances for which no exception to overriding exists, where exceptions require a justification in terms of facts that are provable from the knowledge base. We formally define this semantics and study some semantic and computational properties, where we characterize the complexity of the major reasoning tasks, among them satisfiability testing, instance checking, and conjunctive query answering. Furthermore, we present a translation of extended CKRs with knowledge bases in the Description Logic SROIQ -RL under the novel semantics to datalog programs under the stable model (answer set) semantics. We also present an implementation prototype and examine its scalability with respect to the size of the input CKR and the amount (level) of defeasibility in experiments. Finally, we compare our representation approach with some major formalisms for expressing defeasible knowledge in Description Logics and contextual knowledge representation. Our work adds to the body of results on using deductive database technology such as SQL and datalog in these areas, and provides an expressive formalism (in terms of intrinsic complexity) for exception handling by overriding. [ABSTRACT FROM AUTHOR]

Belief revision of knowledge bases represented by a set of sentences in a given logic has been extensively studied but for specific logics, mainly propositional, and also recently Horn and description logics. Here, we propose to generalize this operation from a model-theoretic point of view, by defining revision in the abstract model theory of satisfaction systems. In this framework, we generalize to any satisfaction system the characterization of the AGM postulates given by Katsuno and Mendelzon for propositional logic in terms of minimal change among interpretations. In this generalization, the constraint on syntax independence is partially relaxed. Moreover, we study how to define revision, satisfying these weakened AGM postulates, from relaxation notions that have been first introduced in description logics to define dissimilarity measures between concepts, and the consequence of which is to relax the set of models of the old belief until it becomes consistent with the new pieces of knowledge. We show how the proposed general framework can be instantiated in different logics such as propositional, first-order, description and Horn logics. In particular for description logics, we introduce several concrete relaxation operators tailored for the description logic ALC and its fragments EL and ELU , discuss their properties and provide some illustrative examples. [ABSTRACT FROM AUTHOR]

• An Image-to-text model NeoDescriber for Neoclassical building description. • Four architectural image databases were built to train visual modules. • Higher BERTScore than BLIP-2 for architectural style description. Architectural style description is important for the renewal and reuse of historical monuments. However, the identification of Neoclassical buildings is more difficult than that of other European architectural styles owing to the revival of classicism and its numerous variants. This paper proposes the image-to-text model NeoDescriber for the automatic identification and description of Neoclassical buildings based on the combination of dedicated visual classification and detection modules organized by expert knowledge in architecture. NeoDescriber takes building façade images as input and follows a coarse-to-fine description logic to generate structured annotations covering the whole building and key building elements. We built several building image datasets composed of more than 300 historical monuments to train and validate different visual modules. The results showed the acceptance performance of both classification and detection modules, with average precisions ranging from 73.6% to 95.2%. The generated text descriptions were then compared with results from BLIP-2 by qualitative and quantitative analyses. With human descriptions as a reference, the results showed that NeoDescriber's generated descriptions were more precise and detailed, having a higher BERTScore for Neoclassical monuments. Thus, NeoDescriber could successfully recognize and describe Neoclassical buildings. [ABSTRACT FROM AUTHOR]

• We proposed a system is based on LiverFibroOnto that describes concepts related to patient symptoms and different risk factors of the Viral hepatitis C virus (HCV). • The proposal of an intelligent clinical DSS system that utilizes fuzzy conceptual representations capabilities, the knowledge contained in the semantic repository, and a rule-based engine. • The proposed system infers the severity of the disease to help the patient to counteract the disease. • We tested the developed system using a real dataset for fibrosis diagnosis. • The performance of the proposed system was compared with that of the now-standard Mamdani fuzzy inference system and demonstrated higher performance, with 97.8% accuracy. The domain of the digestive system is prone to severe chronic disease in the form of liver cirrhosis, which is currently a leading cause of mortality. This article presents a new intelligent system for predicting the severity of liver fibrosis in patients with chronic viral hepatitis C. The proposed system is based on the inference capabilities of fuzzy ontology and operates on semantic rule-based techniques. A fuzzy decision tree technique was employed to generate the ontology rule base using a dataset of real fibrosis cases from the Mansoura University Hospital, Egypt. These rules were then encoded into a set of fuzzy semantic rules using the fuzzy description logic format. To evaluate the system's effectiveness, the proposed ontology was then tested on 47 chronic HCV cases, with an attempt made to see if this correctly diagnosed the patients' conditions. The performance of the proposed system was compared with that of the now-standard Mamdani fuzzy inference system; while the latter achieved an accuracy of 95.7/%, the proposed fuzzy ontology-based system demonstrated higher performance, with 97.8% accuracy. Furthermore, the proposed system also supports semantic interoperability between clinical decision support systems and electronic health record ecosystems. The positive impacts of this system on the correct prediction of liver fibrosis severity thus suggest that it has the potential to assist medical professionals in diagnosing and treating this dangerous disease. [ABSTRACT FROM AUTHOR]

Lightweight description logics are knowledge representation formalisms characterised by the low complexity of their standard reasoning tasks. They have been successfully employed for constructing large ontologies that model domain knowledge in several different practical applications. In order to maintain these ontologies, it is often necessary to detect the axioms that cause a given consequence. This task is commonly known as axiom pinpointing. In this paper, we provide a thorough analysis of the complexity of several decision, counting, and enumeration problems associated to axiom pinpointing in lightweight description logics. [ABSTRACT FROM AUTHOR]

This paper reports on an investigation into the use of ontology technologies to support taxonomic functions. Support for taxonomy is imperative given several recent discussions and publications that voiced concern over the taxonomic impediment within the broader context of the life sciences. Taxonomy is defined as the scientific classification, description and grouping of biological organisms into hierarchies based on sets of shared characteristics, and documenting the principles that enforce such classification. Under taxonomic functions we identified two broad categories: the classification functions concerned with identification and naming of organisms, and secondly classification functions concerned with categorization and revision (i.e. grouping and describing, or revisiting existing groups and descriptions). Ontology technologies within the broad field of artificial intelligence include computational ontologies that are knowledge representation mechanisms using standardized representations that are based on description logics (DLs). This logic base of computational ontologies provides for the computerized capturing and manipulation of knowledge. Furthermore, the set-theoretical basis of computational ontologies ensures particular suitability towards classification, which is considered as a core function of systematics or taxonomy. Using the specific case of Afrotropical bees, this experimental research study represents the taxonomic knowledge base as an ontology, explore the use of available reasoning algorithms to draw the necessary inferences that support taxonomic functions (identification and revision) over the ontology and implement a Web-based application (the WOC). The contributions include the ontology, a reusable and standardized computable knowledge base of the taxonomy of Afrotropical bees, as well as the WOC and the evaluation thereof by experts. [ABSTRACT FROM AUTHOR]

Our understanding of an application domain evolves over time. If we consider an ontology as a set of semantic constraints which describes our understanding of an application domain, ontologies must be revised. Indeed, adding a new semantic constraint to an ontology may make it inconsistent. To restore consistency with minimal loss of semantics, we would change other semantic constraints of the ontology such that the resulting ontology is semantically as close as possible to the initial ontology. To be able to say that an ontology is semantically close to another one, it is needed to define a distance over finite structures representing models, called completion graphs , which characterize the semantics of an ontology. In this paper we present a tableau algorithm for building such completion graphs of an ontology expressed in the description logic SHIQ with individuals. Based on the distance defined over completion graphs, we introduce a revision operation applied to a SHIQ ontology with a set of new semantic constraints. This revision operation computes the completion graphs that a revised ontology should admit. However, there does not always exist an ontology expressible in SHIQ from which a tableau algorithm generates exactly a given set of completion graphs. This leads us to introduce the notion of upper approximation ontology from which a tableau algorithm can generate the smallest set of completion graphs including a given set of completion graphs. This notion allows us to design an algorithm for constructing a revised ontology from an initial ontology with a set of new semantic constraints. We also implement the proposed algorithms with optimizations and report some experimental results to show that a model-based approach to revision of expressive ontologies is practicable. [ABSTRACT FROM AUTHOR]

DL N is a recent nonmonotonic description logic, designed for satisfying independently proposed knowledge engineering requirements, and for removing some recurrent drawbacks of traditional nonmonotonic semantics. In this paper we study the logical properties of DL N and illustrate some of the relationships between the KLM postulates and the characteristic features of DL N , including its novel way of dealing with unresolved conflicts between defeasible axioms. Moreover, we fix a problem affecting the original semantics of DL N and accordingly adapt the reduction from DL N inferences to classical inferences. Along the paper, we use various versions of the KLM postulates to deepen the comparison with related work, and illustrate the different tradeoffs between opposite requirements adopted by each approach. [ABSTRACT FROM AUTHOR]

In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL) and computation-tree logic (CTL). Hierarchical model checking is a model checking paradigm that can appropriately verify systems with hierarchical information and structures. A sequential linear-time temporal logic (sLTL) and a sequential computation-tree logic (sCTL), which can suitably represent hierarchical information and structures, are developed by extending LTL and CTL, respectively. Translations from sLTL and sCTL into LTL and CTL, respectively, are defined, and theorems for embedding sLTL and sCTL into LTL and CTL, respectively, are proved using these translations. These embedding theorems allow us to reuse the standard LTL- and CTL-based model checking algorithms to verify hierarchical systems that are modeled and specified by sLTL and sCTL. [ABSTRACT FROM AUTHOR]

Earth Observation data is of great interest for a wide spectrum of scientific domain applications. An enhanced access to remote sensing images for “domain” experts thus represents a great advance since it allows users to interpret remote sensing images based on their domain expert knowledge. However, such an advantage can also turn into a major limitation if this knowledge is not formalized, and thus is difficult for it to be shared with and understood by other users. In this context, knowledge representation techniques such as ontologies should play a major role in the future of remote sensing applications. We implemented an ontology-based prototype to automatically classify Landsat images based on explicit spectral rules. The ontology is designed in a very modular way in order to achieve a generic and versatile representation of concepts we think of utmost importance in remote sensing. The prototype was tested on four subsets of Landsat images and the results confirmed the potential of ontologies to formalize expert knowledge and classify remote sensing images. [ABSTRACT FROM AUTHOR]

We consider the problem of ontological query answering, that is, the problem of answering a database query (typically a conjunctive query) in the presence of an ontology. This means that during the query answering process we also need to take into account the knowledge that can be inferred from the given database and ontology. Building, however, ontology-aware database systems from scratch, with sophisticated optimization techniques, is a highly non-trivial task that requires a great engineering effort. Therefore, exploiting conventional database systems is an important route towards efficient ontological query answering. Nevertheless, standard database systems are unaware of ontologies. An approach to ontological query answering that enables the use of standard database systems is the so-called polynomial combined query rewriting, originally introduced in the context of description logics: the conjunctive query q and the ontology Σ are rewritten in polynomial time into a first-order query q Σ (in a database-independent way), while the database D and the ontology Σ are rewritten in polynomial time into a new database D Σ (in a query-independent way), such that the answer to q in the presence of Σ over D coincides with the answer to q Σ over D Σ. The latter can then be computed by exploiting a conventional database system. In this work, we focus on linear and guarded existential rules, which form robust rule-based languages for modeling ontologies, and investigate the limits of polynomial combined query rewriting. In particular, we show that this type of rewriting can be successfully applied to (i) linear existential rules when the rewritten query can use the full power of first-order queries, (ii) linear existential rules when the arity of the underlying schema is fixed and the rewritten query is positive existential, namely it uses only existential quantification, conjunction, and disjunction, and (iii) guarded existential rules when the underlying schema is fixed and the rewritten query is positive existential. We can show that the above results reach the limits (under standard complexity-theoretic assumptions such as ▪) of polynomial combined query rewriting in the case of linear and guarded existential rules. [ABSTRACT FROM AUTHOR]