We introduce depth-bounded fuzzy bisimulation between fuzzy Kripke models. Roughly speaking, a depth-bounded fuzzy bisimulation is a decreasing sequence of fuzzy binary relations whose infimum is a fuzzy bisimulation. We provide logical characterizations of depth-bounded fuzzy bisimulations between fuzzy Kripke models w.r.t. a fuzzy multimodal logic fK over complete residuated lattices, including fuzzy invariance of formulas of fK with a modal depth bounded by n under the nth component of a depth-bounded fuzzy bisimulation, as well as the Hennessy-Milner property of depth-bounded fuzzy bisimulations. We also provide a polynomial-time algorithm for computing the nth component of the greatest depth-bounded fuzzy bisimulation between two finite fuzzy Kripke models when the underlying complete residuated lattice is linear.

State reduction of fuzzy automata aims to efficiently construct a suitably small fuzzy automaton equivalent to a given one. It is a significant and well-studied problem in automata theory due to its practical applications in various fields. If we relax the requirement for exact equivalence, then we talk about the approximate state reduction problem, which has gained attention only recently. There are two approaches to approximate state reduction: one seeks approximate equivalence to a specified threshold, while the other aims for exact equivalence for length-bounded words. These two approaches have been considered separately. In this paper, we demonstrate that both approaches, and even their combination, can be achieved by merging indistinguishable states of a fuzzy automaton through the use of sequences of fuzzy relations that we introduce in this paper. We provide characterizations of these sequences, and show that they are closely related to certain approximate simulations for fuzzy automata that emerged in the recent literature. However, their subtle differences significantly affect the process of approximate state reduction. By formally proving this distinction, we generalize some well-known results and offer new insight into approximate state reduction. We discuss how all forms of approximate state reduction can be realized and provide algorithms for calculating the proposed sequences and performing the reductions, along with illustrative examples.

In this article, we introduce fuzzy minimax nets as a novel tool to compute the greatest fuzzy bisimulation/simulation between two finite fuzzy labeled graphs. Fuzzy labeled graphs are a universal data structure for representing fuzzy systems, such as fuzzy automata, fuzzy labeled transition systems, fuzzy Kripke models, fuzzy social networks, and fuzzy interpretations in description logic. The greatest fuzzy bisimulation between two such systems characterizes the similarity between their states, actors, or individuals. Using fuzzy minimax nets, we design the first algorithms for the mentioned computational problems in the case of using the product t-norm, as well as the first algorithms whose complexity order does not depend on the fuzzy values occurring in the inputs for those problems in the case of using the Łukasiewicz t-norm.

Fuzzy description logics (FDLs) are useful for dealing with fuzzy terminological knowledge for domains with linked data. Logical similarity or indiscernibility between individuals with respect to a given FDL is a fuzzy measure, which becomes crisp when the logic is extended with the Baaz projection operator. The measure is closely related to bisimulation. While logical indiscernibility is defined semantically, its corresponding notion based on bisimulation enables the computation. In this article, we study crisp bisimulations between fuzzy interpretations in FDLs with the Baaz projection operator under a general semantics based on an abstract algebra of fuzzy truth values. We define such bisimulations for a large class of FDLs with a rich set of well-known concept and role constructors, including qualified/unqualified number restrictions, nominals and the role constructors that correspond to the program constructors of propositional dynamic logic. We formulate and prove their logical characterizations, including the invariance of concepts under crisp bisimulations and the Hennessy–Milner property of crisp bisimulations. Such logical characterizations do not depend on a concrete semantics, such as the Gödel, Łukasiewicz, and product semantics. Based on crisp bisimulations, we also study indiscernibility of individuals in FDLs with the Baaz projection operator. An interesting consequence of our results states that, when restricting to the considered FDLs and image-finite fuzzy interpretations that are witnessed and modally saturated, indiscernibility of individuals is independent from the underlying algebra of fuzzy truth values in the case without number restrictions, and it is the same for both the Gödel and product semantics in the case with number restrictions.

We provide and prove logical characterizations of fuzzy simulations between fuzzy Kripke models that use a general t-norm-based semantics. We also extend the results for fuzzy Kripke models defined over a general residuated lattice. Our logical characterizations of fuzzy simulations are formulated w.r.t. positive existential fragments of fuzzy propositional dynamic logic without tests and concern fuzzy preservation of positive existential modal formulas under fuzzy simulations as well as the Hennessy-Milner property of fuzzy simulations.

We formulate and prove logical characterizations of crisp simulations and crisp directed simulations between fuzzy labeled transition systems with respect to fuzzy modal logics that use a general t-norm-based semantics. The considered logics are fragments of the fuzzy propositional dynamic logic with the Baaz projection operator. The logical characterizations concern preservation of existential (respectively, positive) modal formulas under crisp simulations (respectively, crisp directed simulations), as well as the Hennessy-Milner property of such simulations.

As a side-effect of the Covid-19 pandemic, significant decreases in medical procedures for noncommunicable diseases have been observed. This calls for a decision support assisting in the analysis of opportunities to relocate procedures among hospitals in an efficient or, preferably, optimal manner. In the current paper we formulate corresponding decision problems and develop linear (mixed integer) programming models for them. Since solving mixed integer programming problems is NP-complete, we verify experimentally their usefulness using real-world data about urological procedures. We show that even for large models, with millions of variables, the problems' instances are solved in perfectly acceptable time.

Bisimulation is a well-known notion in modal logic and the theory of labeled transition systems. It is used for characterizing indiscernibility between states and has important applications in minimizing structures, separating expressive powers of modal and related logics, as well as concept learning in description logics (DLs). Fuzzy bisimulation is a counterpart of bisimulation for dealing with fuzzy structures. In this article, we present an efficient algorithm with a complexity O((m+n)n) for computing the greatest fuzzy bisimulation between two finite fuzzy interpretations in the fuzzy DLfALCunder the Gödel semantics, where n is the number of individuals and m is the number of nonzero instances of roles in the given fuzzy interpretations. We also adapt our algorithm for computing fuzzy bisimulations and simulations between fuzzy finite automata, as well as for dealing with other fuzzy DLs. The resulting algorithms are much more efficient than the previously known ones, as they reduce the complexity from O(n5) to O((m+n)n).

Abstract Berman and Paterson proved that test-free propositional dynamic logic (PDL) is weaker than PDL. One would raise questions: does a similar result also hold for extensions of PDL? For example, is test-free converse-PDL (CPDL) weaker than CPDL? In what circumstances the test operator can be eliminated without reducing the expressive power of a PDL-based logical formalism? These problems have not yet been studied. As the description logics $\mathcal{ALC}_{trans}$ and $\mathcal{ALC}_{reg}$ are, respectively, variants of test-free PDL and PDL, there is a concept of $\mathcal{ALC}_{reg}$ that is not equivalent to any concept of $\mathcal{ALC}_{trans}$. Generalizing this, we prove that there is a concept of $\mathcal{ALC}_{reg}$ that is not equivalent to any concept of the logic that extends $\mathcal{ALC}_{trans}$ with inverse roles, nominals, qualified number restrictions, the universal role and local reflexivity of roles. We also provide some results for the case with RBoxes and TBoxes. One of them states that tests can be eliminated from TBoxes of the deterministic Horn fragment of $\mathcal{ALC}_{reg}$.

Fuzzy description logics (DLs) are extensions of DLs for dealing with imprecise and vague concepts. They found the logical basis for fuzzy ontologies, which are useful for practical applications. Bisimilarity is a natural notion of equivalence between individuals in DLs. In this paper, for the first time, we introduce the notion of bisimilarity in fuzzy DLs under the Zadeh semantics. It is defined using our notion of p-cut simulation between fuzzy interpretations. The considered logics are fuzzy DLs that extend the fuzzy version of the DL ALCreg(a variant of propositional dynamic logic) with features among inverse roles, the universal role, qualified number restrictions, nominals, and local reflexivity of a role. We provide results on preservation of information by the mentioned simulations, conditional invariance of ABoxes and TBoxes by bisimilarity between witnessed interpretations, as well as the Hennessy-Milner property for fuzzy DLs under the Zadeh semantics.

We provide the first algorithm with a polynomial time complexity, O((m + n)2n2), for computing the largest bisimulation-based auto-comparison of a labeled graph in the setting with counting successors, where m is the number of edges and n is the number of vertices. This setting is like the case wit h graded modalities in modal logics and qualified number restrictions in description logics. Furthermore, by using the idea of Henzinger et al. for computing simulations, we give an efficient algorithm, with complexity O((m + n)n), for computing the largest bisimulation-based auto-comparison and the directed similarity relation of a labeled graph in the setting without counting successors. We also adapt our former algorithm for computing the simulation pre-order of a labeled graph in the setting with counting successors.

We propose a method, called QSQN-WF, for evaluating queries to Datalog¬ databases under the well-founded semantics. It is the first one that is set-at-a-time and strictly goal-directed w.r.t. SLS-resolution defined by Przymusinski. These properties are important for reducing accesses to the secondary storage and redundant computations. The first property distinguishes our method from the one based on SLG-resolution by Chen, Swift, and Warren (1995 Chen, W., T. Swift, and D. S. Warren. 1995. Efficient top-down computation of queries under the well-founded semantics. Journal of Logic Programming 24 (3):161–99. doi:10.1016/0743-1066(94)00028-5[Crossref] , [Google Scholar]) (which is tuple-at-a-time). The second property distinguishes our method from the ones based on the magic-sets transformation by Kemp, Srivastava, and Stuckey (1995 Kemp, D. B., D. Srivastava, and P. J. Stuckey. 1995. Bottom-up evaluation and query optimization of well-founded models. Theoretical Computer Science 146 (1 & 2):145–84. doi:10.1016/0304-3975(94)00153-a[Crossref], [Web of Science ®] , [Google Scholar]) and Morishita (1996 Morishita, S. 1996. An extension of Van Gelder's alternating fixpoint to magic programs. Journal of Computer and System Sciences 52 (3):506–21. doi:10.1006/jcss.1996.0038[Crossref], [Web of Science ®] , [Google Scholar]), which use magic atoms not in the most appropriate way and are not strictly goal-directed w.r.t. SLS-resolution. Our method follows SLS-resolution, with Van Gelder’s alternating fixpoint semantics on the background, but uses a query-subquery net to implement tabulation and the set-at-a-time technique, reduce redundant computations, and allow any control strategy within each iteration of the main loop. It is sound and complete w.r.t. the well-founded semantics and has PTIME data complexity.

27

We introduce comparisons with respect to information between interpretations in paraconsistent description logics and use them to define bisimilarity for such logics. As bisimilarity is a natural notion for characterizing indiscernibility in modal and description logics, it is useful for concept learning in description logics also when inconsistencies occur. We give preservation results and the Hennessy-Milner property for comparisons with respect to information in paraconsistent description logics. As consequences, we also obtain invariance results and the Hennessy-Milner property for bisimilarity in paraconsistent description logics.

Combining CPDL (Propositional Dynamic Logic with Converse) and regular grammar logic results in an expressive modal logic denoted by CPDLreg. This logic covers TEAMLOG, a logical formalism used to express properties of agents’ cooperation in terms of beliefs, goals and intentions. It can also be us ed as a description logic for expressing terminological knowledge, in which both regular role inclusion axioms and CPDL-like role constructors are allowed. In this paper, we develop an expressive and tractable rule language called Horn-CPDLreg. As a special property, this rule language allows the concept constructor “universal restriction” to appear on the left hand side of general concept inclusion axioms. We use a special semantics for Horn-CPDLreg that is based on pseudo-interpretations. It is called the constructive semantics and coincides with the traditional semantics when the concept constructor “universal restriction” is disallowed on the left hand side of concept inclusion axioms or when the language is used as an epistemic formalism and the accessibility relations are serial. We provide an algorithm with PTIME data complexity for checking whether a knowledge base in Horn-CPDLreg has a pseudo-model. This shows that the instance checking problem in Horn-CPDLreg with respect to the constructive semantics has PTIME data complexity.

We present the first direct tableau decision procedure for graded PDL, which uses global caching and has ExpTime (optimal) complexity when numbers are encoded in unary. It shows how to combine checking fulfillment of existential star modalities with integer linear feasibility checking for tableaux with global caching. As graded PDL can be used as a description logic for representing and reasoning about terminological knowledge, our procedure is useful for practical applications.

Ontologies have been applied in a wide range of practical domains. They play a key role in data modeling, information integration, and the creation of semantic web services, intelligent web sites and intelligent software agents. The Web ontology language OWL, recommended by W3C, is based on description logics (DLs). Automated reasoning in DLs is very important for the success of OWL, as it provides support for visualization, debugging, and querying of ontologies. The existing ontology reasoners are not yet satisfactory, especially when dealing with qualified number restrictions and large ontologies. In this paper, we present the design of our new reasoner TGC2, which uses tableaux with global caching for reasoning in E xpTime-complete DLs. The characteristic of TGC2 is that it is based on our tableau methods with the optimal ( ExpTime) complexity, while the existing well-known tableau-based reasoners for DLs have a non-optimal complexity (at least NExpTime). We briefly describe the tableau methods used by TGC2. We then provide the design principles of TGC2 and some important optimization techniques for increasing the efficiency of this reasoner. We also present preliminary evaluation results of TGC2. They show that TGC2 deals with qualified number restrictions much better than the other existing reasoners.

We present the first tableau method with an EXPTIME (optimal) complexity for checking satisfiability of a knowledge base in the description logic ${\cal{SHOQ}}$, which extends ${\cal{ALC}}$ with transitive roles, hierarchies of roles, nominals and qualified number restrictions. The complexity is measured using unary representation for numbers (in number restrictions). Our procedure is based on global caching and integer linear feasibility checking.

Concept learning in description logics (DLs) is similar to binary classification in traditional machine learning. The difference is that in DLs objects are described not only by attributes but also by binary relationships between objects. In this pap

We develop a cut-free tableau calculus for the logic CPDLreg, leading to the first cut-free EXPTIME (optimal) tableau decision procedure for CPDLreg. This logic extends Converse-PDL with regular inclusion axioms characterized by finite automata. It is a logical formalism suitable for expressing complex properties of agents' cooperation in terms of beliefs, goals and intentions.

We study Horn fragments of serial multimodal logics which are characterized by regular grammars with converse. Such logics are useful for reasoning about epistemic states of multiagent systems as well as similarity-based approximate reasoning. We provide the first algorithm with PTIME data complexity for checking satisfiability of a Horn knowledge base in a serial regular grammar logic with converse.

We show that global caching can be used with propagation of both satisfiability and unsatisfiability in a sound manner to give an EXPTIME algorithm for checking satisfiability w.r.t. a TBox in the basic description logic ALC. Our algorithm is based on a simple traditional tableau calculus which builds an and-or graph where no two nodes of the graph contain the same formula set. When a duplicate node is about to be created, we use the pre-existing node as a proxy, even if the proxy is from a different branch of the tableau, thereby building global caching into the algorithm from the start. Doing so is important since it allows us to reason explicitly about the correctness of global caching. We then show that propagating both satisfiability and unsatisfiability via the and-or structure of the graph remains sound. In the longer paper, by combining global caching, propagation and cutoffs, our framework reduces the search space more significantly than the framework of [1]. Also, the freedom to use arbitrary search heuristics significantly increases its application potential. A longer version with all optimisations is currently under review for a journal. An extension for SHI will appear in TABLEAUX 2007.

We generalize the QSQR evaluation method to give the first set-oriented depth-first evaluation method for Horn knowledge bases. The resulting procedure closely simulates SLD-resolution (to take advantages of the goal-directed approach) and highly exploits set-at-a-time tabling. Our generalized QSQR evaluation procedure is sound and complete. It does not use adornments and annotations. To deal with function symbols, our procedure uses iterative deepening search, which iteratively increases term-depth bound for atoms and substitutions occurring in the computation. When the term-depth bound is fixed, our evaluation procedure runs in polynomial time in the size of extensional relations.

In natural language we often use graded concepts, reflecting different intensity degrees of certain features. Whenever such concepts appear in a given real-life context, they need to be appropriately expressed in its models. In this paper, we provide

Developing a good formalism and an efficient decision procedure for the instance checking problem is desirable for practical application of description logics. The data complexity of the instance checking problem is coNP-complete even for Horn knowledge bases in the basic description logic ALC. In this paper, we present and study weakenings with PTIME data complexity of the instance checking problem for Horn knowledge bases in regular description logics. We also study cases when the weakenings are an exact approximation. In contrast to previous related work of other authors, our approach deals with the case when the constructor ∀ is allowed in premises of program clauses that are used as terminological axioms.

We reformulate Pratt’s tableau decision procedure of checking satisfiability of a set of formulas in PDL. Our formulation is simpler and its implementation is more direct. Extending the method we give the first ExpTime (optimal) tableau decision procedure not based on transformation for checking consistency of an ABox w.r.t. a TBox in PDL (here, PDL is treated as a description logic). We also prove a new result that the data complexity of the instance checking problem in PDL is coNP-complete.

We develop clausal tableau calculi for six multimodal logics variously designed for reasoning about multi-degree belief, reasoning about distributed systems of belief and for reasoning about epistemic states of agents in multi-agent systems. Our tableau calculi are sound, complete, cut-free and have the analytic superformula property, thereby giving decision procedures for all of these logics. We also use our calculi to obtain complexity results for five of these logics. The complexity of the remaining logic was known.

We report on our implementation of a tableau prover for the description logic ALC, which is based on the EXPTIME tableau algorithm using global caching for ALC that was developed jointly by us and Goré [9]. The prover, called TGC for "Tableaux with Global Caching", checks satisfiability of a set of concepts w.r.t. a set of global assumptions by constructing an and-or graph, using tableau rules for expanding nodes. We have implemented for TGC a special set of optimizations which co-operates very well with global caching and various search strategies. The test results on the test set T98-sat of DL'98 Systems Comparison indicate that TGC is an efficient prover for ALC. This suggests that global caching together with the set of optimizations used for TGC is worth implementing and experimenting also for other modal/description logics.

We give algorithms to construct the least L-model for a given positive modal logic program P, where L can be one of the modal logics KD, T, KDB, B, KD4, S4, KD5, KD45, and S5. If L ∈ {KD5,KD45,S5}, or L ∈ {KD,T,KDB,B} and the modal depth of P is finitely bounded, then the least L-model of P can be constructed in PTIME and coded in polynomial space. We also show that if P has no flat models then it has the least models in KB, K5, K45, and KB5. As a consequence, the problem of checking the satisfiability of a set of modal Horn formulae with finitely bounded modal depth in KD, T, KB, KDB, or B is decidable in PTIME. The known result that the problem of checking the satisfiability of a set of Horn formulae in K5, KD5, K45, KD45, KB5, or S5 is decidable in PTIME is also studied in this work via a different method.