ﻻ يوجد ملخص باللغة العربية
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).
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
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
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
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 s
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