Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA set-based reasoner for the description logic $shdlssx$ (Extended Version)
95
0
0.0
(
0
)
Added by
Daniele Francesco Santamaria
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We present a ke-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic $dlssx$ ($shdlssx$, for short). Our application solves the main TBox and ABox reasoning problems for $shdlssx$. In particular, it solves the consistency problem for $shdlssx$-knowledge bases represented in set-theoretic terms, and a generalization of the emph{Conjunctive Query Answering} problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and optimizes a previous prototype for the consistency checking of $shdlssx$-knowledge bases (see cite{cilc17}), is implemented in textsf{C++}. It supports $shdlssx$-knowledge bases serialized in the OWL/XML format, and it admits also rules expressed in SWRL (Semantic Web Rule Language).
rate research
Read More
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 study a conservative extension of classical propositional logic distinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or classical. Proofs of strong propositions must be constructive in some sense, whereas proofs of classical propositions proceed by contradiction. The system, in natural deduction style, is shown to be sound and complete with respect to a Kripke semantics. We develop the system from the perspective of the propositions-as-types correspondence by deriving a term assignment system with confluent reduction. The proof of strong normalization relies on a translation to System F with Mendler-style recursion.
We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study extensions of the points-to fragment of symbolic-heap separation logic with various forms of Presburger arithmetic constraints. Most significantly, we find that, even in the minimal case when we allow only conjunctions of simple difference constraints (xleq x+k) where k is an integer, polynomial-time decidability is already impossible: satisfiability becomes NP-complete, while quantifier-free entailment becomes coNP-complete and quantified entailment becomes P2-complete (P2 is the second class in the polynomial-time hierarchy) In fact we prove that the upper bound is the same, P2, even for the full pointer arithmetic but with a fixed pointer offset, where we allow any Boolean combinations of the elementary formulas (x=x+k0), (xleq x+k0), and (x<x+k0), and, in addition to the points-to formulas, we allow spatial formulas of the arrays the length of which is bounded by k0 and lists which length is bounded by k0, etc, where k0 is a fixed integer. However, if we allow a significantly more expressive form of pointer arithmetic - namely arbitrary Boolean combinations of elementary formulas over arbitrary pointer sums - then the complexity increase is relatively modest for satisfiability and quantifier-free entailment: they are still NP-complete and coNP-complete respectively, and the complexity appears to increase drastically for quantified entailments.
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.
This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that Vampire is correct and use this to motivate future challenges that need to be addressed to make this process more straightforward and to achieve better correctness guarantees.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
