Domenico Cantone

An optimized KE-tableau-based system for reasoning in the description logic $\shdlssx$ (Extended Version)

2018 · arXiv (Cornell University)

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 …

The Many Qualities of a New Directly Accessible Compression Scheme

2023 · arXiv (Cornell University)

We present a new variable-length computation-friendly encoding scheme, named SFDC (Succinct Format with Direct aCcesibility), that supports direct and fast accessibility to any element of the compressed sequence and achieves compression ratios often higher than …

Decision algorithms for fragments of real analysis. II. A theory of differentiable functions with convexity and concavity predicates

2024 · arXiv (Cornell University)

We address the decision problem for a fragment of real analysis involving differentiable functions with continuous first derivatives. The proposed theory, besides the operators of Tarski's theory of reals, includes predicates for comparisons, monotonicity, convexity, …