PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 7

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Horn Knowledge Bases in Regular Description Logics with PTIME Data Complexity
Nguyen L.A. L.A.
Fundamenta Informaticae
|
2010
|
Vol. 104, nr 4
349-384
EN
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 descriptionn 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.
2
Content available remote Checking Consistency of an ABox w.r.t. Global Assumptions in PDL
Nguyen L.A. L.A., Szałas A.
Fundamenta Informaticae
|
2010
|
Vol. 102, nr 1
97-113
EN
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.
3
Content available remote A Framework for Graded Beliefs, Goals and Intentions
Dunin-Kęplicz B., Nguyen L.A. L.A., Szałas A.
Fundamenta Informaticae
|
2010
|
Vol. 100, nr 1/4
53-76
EN
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 a framework which allows for extending the BGI model of agency by grading beliefs, goals and intentions. We concentrate on TEAMLOG [6, 7, 8, 9, 12] and provide a complexity-optimal decision method for its graded version TEAMLOGK by translating it into CPDL_reg (propositional dynamic logic with converse and "inclusion axioms" characterized by regular languages). We also develop a tableau calculus which leads to the first EXPTIME (optimal) tableau decision procedure for CPDL_reg. As CPDL_reg is suitable for expressing complex properties of graded operators, the procedure can also be used as a decision tool for other multiagent formalisms.
4
Content available remote Clausal Tableaux for Multimodal Logics of Belief
Goré R., Nguyen L.A. L.A.
Fundamenta Informaticae
|
2009
|
Vol. 94, nr 1
21-40
EN
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.
5
Content available remote An Efficient Tableau Prover using Global Caching for the Description Logic ALC
Nguyen L.A. L.A.
Fundamenta Informaticae
|
2009
|
Vol. 93, nr 1-3
273-288
EN
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´e [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.
6
Content available remote Foundations of Modal Deductive Databases
Nguyen L.A. L.A.
Fundamenta Informaticae
|
2007
|
Vol. 79, nr 1-2
85-135
EN
We give formulations for modal deductive databases and present a modal query language called MDatalog. We define modal relational algebras and give the seminaive evaluation algorithm, the top-down evaluation algorithm, and the magic-set transformation for MDatalog queries. The results of this paper like soundness and completeness of the top-down evaluation algorithm or correctness of the magic-set transformation are proved for the multimodal logics of belief KDI4s5, KDI45, KD4s5s, KD45(m), KD4Ig5a, and the class of serial context-free grammar logics. We also show that MDatalog has PTIME data complexity in the logics KDI4s5, KDI45, KD4s5s, and KD45(m).
7
Content available remote Negative Ordered Hyper-Resolution as a Proof Procedure for Disjunctive Logic Programming
Nguyen L.A. L.A.
Fundamenta Informaticae
|
2006
|
Vol. 70, nr 4
351-366
EN
We prove that negative hyper-resolution using any liftable and well-founded ordering refinement is a sound and complete procedure for answering queries in disjunctive logic programs. In our formulation, answers of queries are defined using disjunctive substitutions, which are more flexible than answer literals used in theorem proving systems.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.