Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDeciding SHACL Shape Containment through Description Logics Reasoning (Extended Version)
84
0
0.0
(
0
)
Added by
Martin Leinberger
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
The Shapes Constraint Language (SHACL) allows for formalizing constraints over RDF data graphs. A shape groups a set of constraints that may be fulfilled by nodes in the RDF graph. We investigate the problem of containment between SHACL shapes. One shape is contained in a second shape if every graph node meeting the constraints of the first shape also meets the constraints of the second. To decide shape containment, we map SHACL shape graphs into description logic axioms such that shape containment can be answered by description logic reasoning. We identify several, increasingly tight syntactic restrictions of SHACL for which this approach becomes sound and complete.
rate research
Read More
We study query containment in three closely related formalisms: monadic disjunctive Datalog (MDDLog), MMSNP (a logical generalization of constraint satisfaction problems), and ontology-mediated queries (OMQs) based on expressive description logics and unions of conjunctive queries. Containment in MMSNP was known to be decidable due to a result by Feder and Vardi, but its exact complexity has remained open. We prove 2NEXPTIME-completeness and extend this result to monadic disjunctive Datalog and to OMQs.
The paper is focused on temporal logics for the description of the behaviour of real-time pushdown reactive systems. The paper is motivated to bridge tractable logics specialized for expressing separately dense-time real-time properties and context-free properties by ensuring decidability and tractability in the combined setting. To this end we introduce two real-time linear temporal logics for specifying quantitative timing context-free requirements in a pointwise semantics setting: Event-Clock Nested Temporal Logic (ECNTL) and Nested Metric Temporal Logic (NMTL). The logic ECNTL is an extension of both the logic CARET (a context-free extension of standard LTL) and Event-Clock Temporal Logic (a tractable real-time logical framework related to the class of Event-Clock automata). We prove that satisfiability of ECNTL and visibly model-checking of Visibly Pushdown Timed Automata VPTA against ECNTL are decidable and EXPTIME-complete. The other proposed logic NMTL is a context-free extension of standard Metric Temporal Logic (MTL). It is well known that satisfiability of future MTL is undecidable when interpreted over infinite timed words but decidable over finite timed words. On the other hand, we show that by augmenting future MTL with future context-free temporal operators, the satisfiability problem turns out to be undecidable also for finite timed words. On the positive side, we devise a meaningful and decidable fragment of the logic NMTL which is expressively equivalent to ECNTL and for which satisfiability and visibly model-checking of VPTA are EXPTIME-complete.
We present a ke-based procedure for the main TBox and ABox reasoning tasks for the description logic $dlssx$, in short $shdlssx$. The logic $shdlssx$, representable in the decidable multi-sorted quantified set-theoretic fragment $flqsr$, combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics. %In fact it supports, among other features, Boolean operations on concepts and roles, role constructs such as the product of concepts and role chains on the left hand side of inclusion axioms, and role properties such as transitivity, symmetry, reflexivity, and irreflexivity. Our algorithm is based on a variant of the kespace system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the $gamma$-rule. The novel system, called keg, turns out to be an improvement of the system introduced in cite{RR2017} and of standard first-order ke x cite{dagostino94}. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that the performances of the keg-based reasoner are often up to about 400% better than the ones of the other two systems. This a first step towards the construction of efficient reasoners for expressive OWL ontologies based on fragments of computable set-theory.
We consider multi-agent systems where agents actions and beliefs are determined aleatorically, or by the throw of dice. This system consists of possible worlds that assign distributions to independent random variables, and agents who assign probabilities to these possible worlds. We present a novel syntax and semantics for such system, and show that they generalise Modal Logic. We also give a sound and complete calculus for reasoning in the base semantics, and a sound calculus for the full modal semantics, that we conjecture to be complete. Finally we discuss some application to reasoning about game playing agents.
It is a strength of graph-based data formats, like RDF, that they are very flexible with representing data. To avoid run-time errors, program code that processes highly-flexible data representations exhibits the difficulty that it must always include the most general case, in which attributes might be set-valued or possibly not available. The Shapes Constraint Language (SHACL) has been devised to enforce constraints on otherwise random data structures. We present our approach, Type checking using SHACL (TyCuS), for type checking code that queries RDF data graphs validated by a SHACL shape graph. To this end, we derive SHACL shapes from queries and integrate data shapes and query shapes as types into a $lambda$-calculus. We provide the formal underpinnings and a proof of type safety for TyCuS. A programmer can use our method in order to process RDF data with simplified, type checked code that will not encounter run-time errors (with usual exceptions as type checking cannot prevent accessing empty lists).
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
