-
Longest Common Substring and Longest Palindromic Substring in $\tilde{\mathcal{O}}(\sqrt{n})$ Time
Authors:
Domenico Cantone,
Simone Faro,
Arianna Pavone,
Caterina Viola
Abstract:
The Longest Common Substring (LCS) and Longest Palindromic Substring (LPS) are classical problems in computer science, representing fundamental challenges in string processing. Both problems can be solved in linear time using a classical model of computation, by means of very similar algorithms, both relying on the use of suffix trees. Very recently, two sublinear algorithms for LCS and LPS in the…
▽ More
The Longest Common Substring (LCS) and Longest Palindromic Substring (LPS) are classical problems in computer science, representing fundamental challenges in string processing. Both problems can be solved in linear time using a classical model of computation, by means of very similar algorithms, both relying on the use of suffix trees. Very recently, two sublinear algorithms for LCS and LPS in the quantum query model have been presented by Le Gall and Seddighin~\cite{GallS23}, requiring $\tilde{\mathcal{O}}(n^{5/6})$ and $\tilde{\mathcal{O}}(\sqrt{n})$ queries, respectively. However, while the query model is fascinating from a theoretical standpoint, its practical applicability becomes limited when it comes to crafting algorithms meant for actual execution on real hardware. In this paper we present, for the first time, a $\tilde{\mathcal{O}}(\sqrt{n})$ quantum algorithm for both LCS and LPS working in the circuit model of computation. Our solutions are simpler than previous ones and can be easily translated into quantum procedures. We also present actual implementations of the two algorithms as quantum circuits working in $\mathcal{O}(\sqrt{n}\log^5(n))$ and $\mathcal{O}(\sqrt{n}\log^4(n))$ time, respectively.
△ Less
Submitted 3 September, 2023;
originally announced September 2023.
-
Quantum Circuits for Fixed Substring Matching Problems
Authors:
Domenico Cantone,
Simone Faro,
Arianna Pavone,
Caterina Viola
Abstract:
Quantum computation represents a computational paradigm whose distinctive attributes confer the ability to devise algorithms with asymptotic performance levels significantly superior to those achievable via classical computation. Recent strides have been taken to apply this computational framework in tackling and resolving various issues related to text processing. The resultant solutions demonstr…
▽ More
Quantum computation represents a computational paradigm whose distinctive attributes confer the ability to devise algorithms with asymptotic performance levels significantly superior to those achievable via classical computation. Recent strides have been taken to apply this computational framework in tackling and resolving various issues related to text processing. The resultant solutions demonstrate marked advantages over their classical counterparts. This study employs quantum computation to efficaciously surmount text processing challenges, particularly those involving string comparison. The focus is on the alignment of fixed-length substrings within two input strings. Specifically, given two input strings, $x$ and $y$, both of length $n$, and a value $d \leq n$, we want to verify the following conditions: the existence of a common prefix of length $d$, the presence of a common substring of length $d$ beginning at position $j$ (with $0 \leq j < n$) and, the presence of any common substring of length $d$ beginning in both strings at the same position. Such problems find applications as sub-procedures in a variety of problems concerning text processing and sequence analysis. Notably, our approach furnishes polylogarithmic solutions, a stark contrast to the linear complexity inherent in the best classical alternatives.
△ Less
Submitted 22 August, 2023;
originally announced August 2023.
-
The Ontology for Agents, Systems and Integration of Services: OASIS version 2
Authors:
Giampaolo Bella,
Domenico Cantone,
Carmelo Fabio Longo,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
Semantic representation is a key enabler for several application domains, and the multi-agent systems realm makes no exception. Among the methods for semantically representing agents, one has been essentially achieved by taking a behaviouristic vision, through which one can describe how they operate and engage with their peers. The approach essentially aims at defining the operational capabilities…
▽ More
Semantic representation is a key enabler for several application domains, and the multi-agent systems realm makes no exception. Among the methods for semantically representing agents, one has been essentially achieved by taking a behaviouristic vision, through which one can describe how they operate and engage with their peers. The approach essentially aims at defining the operational capabilities of agents through the mental states related with the achievement of tasks. The OASIS ontology -- An Ontology for Agent, Systems, and Integration of Services, presented in 2019 -- pursues the behaviouristic approach to deliver a semantic representation system and a communication protocol for agents and their commitments. This paper reports on the main modeling choices concerning the representation of agents in OASIS 2, the latest major upgrade of OASIS, and the achievement reached by the ontology since it was first introduced, in particular in the context of ontologies for blockchains.
△ Less
Submitted 20 February, 2024; v1 submitted 14 June, 2023;
originally announced June 2023.
-
The Many Qualities of a New Directly Accessible Compression Scheme
Authors:
Domenico Cantone,
Simone Faro
Abstract:
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 those offered by other solutions in the literature. The SFDC scheme provides a flexible and simple representation geared towards either pr…
▽ More
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 those offered by other solutions in the literature. The SFDC scheme provides a flexible and simple representation geared towards either practical efficiency or compression ratios, as required. For a text of length $n$ over an alphabet of size $σ$ and a fixed parameter $λ$, the access time of the proposed encoding is proportional to the length of the character's code-word, plus an expected $\mathcal{O}((F_{σ- λ+ 3} - 3)/F_{σ+1})$ overhead, where $F_j$ is the $j$-th number of the Fibonacci sequence. In the overall it uses $N+\mathcal{O}\big(n \left(λ- (F_{σ+3}-3)/F_{σ+1}\big) \right) = N + \mathcal{O}(n)$ bits, where $N$ is the length of the encoded string. Experimental results show that the performance of our scheme is, in some respects, comparable with the performance of DACs and Wavelet Tees, which are among of the most efficient schemes. In addition our scheme is configured as a \emph{computation-friendly compression} scheme, as it counts several features that make it very effective in text processing tasks. In the string matching problem, that we take as a case study, we experimentally prove that the new scheme enables results that are up to 29 times faster than standard string-matching techniques on plain texts.
△ Less
Submitted 31 March, 2023;
originally announced March 2023.
-
Complexity assessments for decidable fragments of Set Theory. IV: A quadratic reduction of constraints over nested sets to Boolean formulae
Authors:
Domenico Cantone,
Andrea De Domenico,
Pietro Maugeri,
Eugenio G. Omodeo
Abstract:
As a contribution to quantitative set-theoretic inferencing, a translation is proposed of conjunctions of literals of the forms $x=y\setminus z$, $x \neq y\setminus z$, and $z =\{x\}$, where $x,y,z$ stand for variables ranging over the von Neumann universe of sets, into unquantified Boolean formulae of a rather simple conjunctive normal form. The formulae in the target language involve variables r…
▽ More
As a contribution to quantitative set-theoretic inferencing, a translation is proposed of conjunctions of literals of the forms $x=y\setminus z$, $x \neq y\setminus z$, and $z =\{x\}$, where $x,y,z$ stand for variables ranging over the von Neumann universe of sets, into unquantified Boolean formulae of a rather simple conjunctive normal form. The formulae in the target language involve variables ranging over a Boolean ring of sets, along with a difference operator and relators designating equality, non-disjointness and inclusion. Moreover, the result of each translation is a conjunction of literals of the forms $x=y\setminus z$, $x\neq y\setminus z$ and of implications whose antecedents are isolated literals and whose consequents are either inclusions (strict or non-strict) between variables, or equalities between variables. Besides reflecting a simple and natural semantics, which ensures satisfiability-preservation, the proposed translation has quadratic algorithmic time-complexity, and bridges two languages both of which are known to have an NP-complete satisfiability problem.
△ Less
Submitted 12 November, 2022; v1 submitted 9 December, 2021;
originally announced December 2021.
-
On the Convexity of a Fragment of Pure Set Theory with Applications within a Nelson-Oppen Framework
Authors:
Domenico Cantone,
Andrea De Domenico,
Pietro Maugeri
Abstract:
The Satisfiability Modulo Theories (SMT) issue concerns the satisfiability of formulae from multiple background theories, usually expressed in the language of first-order predicate logic with equality. SMT solvers are often based on variants of the Nelson-Oppen combination method, a solver for the quantifier-free fragment of the combination of theories with disjoint signatures, via cooperation am…
▽ More
The Satisfiability Modulo Theories (SMT) issue concerns the satisfiability of formulae from multiple background theories, usually expressed in the language of first-order predicate logic with equality. SMT solvers are often based on variants of the Nelson-Oppen combination method, a solver for the quantifier-free fragment of the combination of theories with disjoint signatures, via cooperation among their decision procedures. When each of the theories to be combined by the Nelson-Oppen method is convex (that is, any conjunction of its literals can imply a disjunction of equalities only when it implies at least one of the equalities) and decidable in polynomial time, the running time of the combination procedure is guaranteed to be polynomial in the size of the input formula. In this paper, we prove the convexity of a fragment of Zermelo-Fraenkel set theory, called Multi-Level Syllogistic, most of whose polynomially decidable fragments we have recently characterized.
△ Less
Submitted 16 September, 2021;
originally announced September 2021.
-
Blockchains through ontologies: the case study of the Ethereum ERC721 standard in OASIS (Extended Version)
Authors:
Giampaolo Bella,
Domenico Cantone,
Cristiano Longo,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
Blockchains are gaining momentum due to the interest of industries and people in \emph{decentralized applications} (Dapps), particularly in those for trading assets through digital certificates secured on blockchain, called tokens. As a consequence, providing a clear unambiguous description of any activities carried out on blockchains has become crucial, and we feel the urgency to achieve that des…
▽ More
Blockchains are gaining momentum due to the interest of industries and people in \emph{decentralized applications} (Dapps), particularly in those for trading assets through digital certificates secured on blockchain, called tokens. As a consequence, providing a clear unambiguous description of any activities carried out on blockchains has become crucial, and we feel the urgency to achieve that description at least for trading. This paper reports on how to leverage the \emph{Ontology for Agents, Systems, and Integration of Services} ("\ONT{}") as a general means for the semantic representation of smart contracts stored on blockchain as software agents. Special attention is paid to non-fungible tokens (NFTs), whose management through the ERC721 standard is presented as a case study.
△ Less
Submitted 20 February, 2024; v1 submitted 7 September, 2021;
originally announced September 2021.
-
Text Searching Allowing for Non-Overlap** Adjacent Unbalanced Translocations
Authors:
Domenico Cantone,
Simone Faro,
Arianna Pavone
Abstract:
In this paper we investigate the \emph{approximate string matching problem} when the allowed edit operations are \emph{non-overlap** unbalanced translocations of adjacent factors}. Such kind of edit operations take place when two adjacent sub-strings of the text swap, resulting in a modified string. The two involved substrings are allowed to be of different lengths.
Such large-scale modificati…
▽ More
In this paper we investigate the \emph{approximate string matching problem} when the allowed edit operations are \emph{non-overlap** unbalanced translocations of adjacent factors}. Such kind of edit operations take place when two adjacent sub-strings of the text swap, resulting in a modified string. The two involved substrings are allowed to be of different lengths.
Such large-scale modifications on strings have various applications. They are among the most frequent chromosomal alterations, accounted for 30\% of all losses of heterozygosity, a major genetic event causing inactivation of cancer suppressor genes. In addition, among other applications, they are frequent modifications accounted in musical or in natural language information retrieval. However, despite of their central role in so many fields of text processing, little attention has been devoted to the problem of matching strings allowing for this kind of edit operation.
In this paper we present three algorithms for solving the problem, all of them with a $\bigO(nm^3)$ worst-case and a $\bigO(m^2)$-space complexity, where $m$ and $n$ are the length of the pattern and of the text, respectively. %
In particular, our first algorithm is based on the dynamic-programming approach. Our second solution improves the previous one by making use of the Directed Acyclic Word Graph of the pattern. Finally our third algorithm is based on an alignment procedure. We also show that under the assumptions of equiprobability and independence of characters, our second algorithm has a $\bigO(n\log^2_σ m)$ average time complexity, for an alphabet of size $σ\geq 4$.
△ Less
Submitted 3 January, 2021;
originally announced January 2021.
-
Ontological Smart Contracts in OASIS: Ontology for Agents, Systems, and Integration of Services (Extended Version)
Authors:
Domenico Cantone,
Carmelo Fabio Longo,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria,
Corrado Santoro
Abstract:
In this contribution we extend an ontology for modelling agents and their interactions, called Ontology for Agents, Systems, and Integration of Services (in short, OASIS), with conditionals and ontological smart contracts (in short, OSCs). OSCs are ontological representations of smart contracts that allow to establish responsibilities and authorizations among agents and set agreements, whereas con…
▽ More
In this contribution we extend an ontology for modelling agents and their interactions, called Ontology for Agents, Systems, and Integration of Services (in short, OASIS), with conditionals and ontological smart contracts (in short, OSCs). OSCs are ontological representations of smart contracts that allow to establish responsibilities and authorizations among agents and set agreements, whereas conditionals allow one to restrict and limit agent interactions, define activation mechanisms that trigger agent actions, and define constraints and contract terms on OSCs. Conditionals and OSCs, as defined in OASIS, are applied to extend with ontological capabilities digital public ledgers such as the blockchain and smart contracts implemented on it. We will also sketch the architecture of a framework based on the OASIS definition of OSCs that exploits the Ethereum platform and the Interplanetary File System.
△ Less
Submitted 20 February, 2024; v1 submitted 2 December, 2020;
originally announced December 2020.
-
Sequence Searching Allowing for Non-Overlap** Adjacent Unbalanced Translocations
Authors:
Domenico Cantone,
Simone Faro,
Arianna Pavone
Abstract:
Unbalanced translocations are among the most frequent chromosomal alterations, accounted for 30\% of all losses of heterozygosity, a major genetic event causing inactivation of tumor suppressor genes. Despite of their central role in genomic sequence analysis, little attention has been devoted to the problem of matching sequences allowing for this kind of chromosomal alteration. In this paper we i…
▽ More
Unbalanced translocations are among the most frequent chromosomal alterations, accounted for 30\% of all losses of heterozygosity, a major genetic event causing inactivation of tumor suppressor genes. Despite of their central role in genomic sequence analysis, little attention has been devoted to the problem of matching sequences allowing for this kind of chromosomal alteration. In this paper we investigate the \emph{approximate string matching} problem when the edit operations are non-overlap** unbalanced translocations of adjacent factors. In particular, we first present a $O(nm^3)$-time and $O(m^2)$-space algorithm based on the dynamic-programming approach. Then we improve our first result by designing a second solution which makes use of the Directed Acyclic Word Graph of the pattern. In particular, we show that under the assumptions of equiprobability and independence of characters, our algorithm has a $O(n\log^2_σ m)$ average time complexity, for an alphabet of size $σ$, still maintaining the $O(nm^3)$-time and the $O(m^2)$-space complexity in the worst case. To the best of our knowledge this is the first solution in literature for the approximate string matching problem allowing for unbalanced translocations of factors.
△ Less
Submitted 2 December, 2018;
originally announced December 2018.
-
Encoding Sets as Real Numbers (Extended version)
Authors:
Domenico Cantone,
Alberto Policriti
Abstract:
We study a variant of the Ackermann encoding $\mathbb{N}(x) := \sum_{y\in x}2^{\mathbb{N}(y)}$ of the hereditarily finite sets by the natural numbers, applicable to the larger collection $\mathsf{HF}^{1/2}$ of the hereditarily finite hypersets. The proposed variation is obtained by simply placing a `minus' sign before each exponent in the definition of $\mathbb{N}$, resulting in the expression…
▽ More
We study a variant of the Ackermann encoding $\mathbb{N}(x) := \sum_{y\in x}2^{\mathbb{N}(y)}$ of the hereditarily finite sets by the natural numbers, applicable to the larger collection $\mathsf{HF}^{1/2}$ of the hereditarily finite hypersets. The proposed variation is obtained by simply placing a `minus' sign before each exponent in the definition of $\mathbb{N}$, resulting in the expression $\mathbb{R}(x) := \sum_{y\in x}2^{-\mathbb{R}(y)}$. By a careful analysis, we prove that the encoding $\mathbb{R}_{A}$ is well-defined over the whole collection $\mathsf{HF}^{1/2}$, as it allows one to univocally assign a real-valued code to each hereditarily finite hyperset. We also address some preliminary cases of the injectivity problem for $\mathbb{R}_{A}$.
△ Less
Submitted 25 June, 2018;
originally announced June 2018.
-
A set-based reasoner for the description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ (Extended Version)
Authors:
Domenico Cantone,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short). Our application solves the main TBox and ABox reasoning problems for $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. In particular, it solv…
▽ More
We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short). Our application solves the main TBox and ABox reasoning problems for $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. In particular, it solves the consistency problem for $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-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 $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases (see \cite{cilc17}), is implemented in \textsf{C++}. It supports $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases serialized in the OWL/XML format, and it admits also rules expressed in SWRL (Semantic Web Rule Language).
△ Less
Submitted 20 February, 2024; v1 submitted 18 May, 2018;
originally announced May 2018.
-
An optimized KE-tableau-based system for reasoning in the description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ (Extended Version)
Authors:
Domenico Cantone,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$, in short $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. The logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, representable in the decidable multi-sorted quantified set-theoretic fragment $\mathsf{4LQS^R}$, combines the high scal…
▽ More
We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$, in short $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. The logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, representable in the decidable multi-sorted quantified set-theoretic fragment $\mathsf{4LQS^R}$, combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics.
Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the $γ$-rule. The novel system, called KE$^γ$-tableau, turns out to be an improvement of the system introduced in \cite{RR2017} and of standard first-order KE-tableau \cite{dagostino94}. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that the performances of the KE$^γ$-tableau-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.
△ Less
Submitted 20 February, 2024; v1 submitted 27 April, 2018;
originally announced April 2018.
-
A Dual Tableau-based Decision Procedure for a Relational Logic with the Universal Relation (Extended Version)
Authors:
Domenico Cantone,
Marianna Nicolosi-Asmundo,
Ewa Orłowska
Abstract:
We present a first result towards the use of entailment in- side relational dual tableau-based decision procedures. To this end, we introduce a fragment of RL(1) which admits a restricted form of composition, (R ; S) or (R ; 1), where the left subterm R of (R ; S) is only allowed to be either the constant 1, or a Boolean term neither containing the complement operator nor the constant 1, while in…
▽ More
We present a first result towards the use of entailment in- side relational dual tableau-based decision procedures. To this end, we introduce a fragment of RL(1) which admits a restricted form of composition, (R ; S) or (R ; 1), where the left subterm R of (R ; S) is only allowed to be either the constant 1, or a Boolean term neither containing the complement operator nor the constant 1, while in the case of (R ; 1), R can only be a Boolean term involving relational variables and the operators of intersection and of union. We prove the decidability of the fragment by defining a dual tableau- based decision procedure with a suitable blocking mechanism and where the rules to decompose compositional formulae are modified so to deal with the constant 1 while preserving termination. The fragment properly includes the logics presented in previous work and, therefore, it allows one to express, among others, the multi-modal logic K with union and intersection of accessibility relations, and the description logic ALC with union and intersection of roles.
△ Less
Submitted 21 February, 2018;
originally announced February 2018.
-
The Shape of a Benedictine Monastery: The SaintGall Ontology (Extended Version)
Authors:
Claudia Cantale,
Domenico Cantone,
Manuela Lupica Rinato,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
We present an OWL 2 ontology representing the Saint Gall plan, one of the most ancient documents arrived intact to us, which describes the ideal model of a Benedictine monastic complex that inspired the design of many European monasteries.
We present an OWL 2 ontology representing the Saint Gall plan, one of the most ancient documents arrived intact to us, which describes the ideal model of a Benedictine monastic complex that inspired the design of many European monasteries.
△ Less
Submitted 20 February, 2024; v1 submitted 8 September, 2017;
originally announced September 2017.
-
The Satisfiability Problem for Boolean Set Theory with a Choice Correspondence
Authors:
Domenico Cantone,
Alfio Giarlotta,
Stephen Watson
Abstract:
Given a set U of alternatives, a choice (correspondence) on U is a contractive map c defined on a family Omega of nonempty subsets of U. Semantically, a choice c associates to each menu A in Omega a nonempty subset c(A) of A comprising all elements of A that are deemed selectable by an agent. A choice on U is total if its domain is the powerset of U minus the empty set, and partial otherwise. Ac…
▽ More
Given a set U of alternatives, a choice (correspondence) on U is a contractive map c defined on a family Omega of nonempty subsets of U. Semantically, a choice c associates to each menu A in Omega a nonempty subset c(A) of A comprising all elements of A that are deemed selectable by an agent. A choice on U is total if its domain is the powerset of U minus the empty set, and partial otherwise. According to the theory of revealed preferences, a choice is rationalizable if it can be retrieved from a binary relation on U by taking all maximal elements of each menu. It is well-known that rationalizable choices are characterized by the satisfaction of suitable axioms of consistency, which codify logical rules of selection within menus. For instance, WARP (Weak Axiom of Revealed Preference) characterizes choices rationalizable by a transitive relation. Here we study the satisfiability problem for unquantified formulae of an elementary fragment of set theory involving a choice function symbol c, the Boolean set operators and the singleton, the equality and inclusion predicates, and the propositional connectives. In particular, we consider the cases in which the interpretation of c satisfies any combination of two specific axioms of consistency, whose conjunction is equivalent to WARP. In two cases we prove that the related satisfiability problem is NP-complete, whereas in the remaining cases we obtain NP-completeness under the additional assumption that the number of choice terms is constant.
△ Less
Submitted 7 September, 2017;
originally announced September 2017.
-
Extending rational choice behavior: The decision problem for Boolean set theory with a choice correspondence
Authors:
Domenico Cantone,
Alfio Giarlotta,
Pietro Maugeri,
Stephen Watson
Abstract:
Given the family $P$ of all nonempty subsets of a set $U$ of alternatives, a choice over $U$ is a function $c \colon Ω\to P$ such that $Ω\subseteq P$ and $c(B) \subseteq B$ for all menus $B \in Ω$. A choice is total if $Ω= P$, and partial otherwise. In economics, an agent is considered rational whenever her choice behavior satisfies suitable axioms of consistency, which are properties quantified o…
▽ More
Given the family $P$ of all nonempty subsets of a set $U$ of alternatives, a choice over $U$ is a function $c \colon Ω\to P$ such that $Ω\subseteq P$ and $c(B) \subseteq B$ for all menus $B \in Ω$. A choice is total if $Ω= P$, and partial otherwise. In economics, an agent is considered rational whenever her choice behavior satisfies suitable axioms of consistency, which are properties quantified over menus. Here we address the following lifting problem: Given a partial choice satisfying one or more axioms of consistency, is it possible to extend it to a total choice satisfying the same axioms? After characterizing the lifting of some choice properties that are well-known in the economics literature, we study the decidability of the connected satisfiability problem for unquantified formulae of an elementary fragment of set theory, which involves a choice function symbol, the Boolean set operators, the singleton, the equality and inclusion predicates, and the propositional connectives. In two cases we prove that the satisfiability problem is NP-complete, whereas in the remaining cases we obtain NP-completeness under the additional assumption that the number of choice terms is constant.
△ Less
Submitted 2 December, 2022; v1 submitted 21 August, 2017;
originally announced August 2017.
-
A C++ reasoner for the description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ (Extended Version)
Authors:
Domenico Cantone,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
We present an ongoing implementation of a KE-tableau based reasoner for a decidable fragment of stratified elementary set theory expressing the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ (shortly $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$). The reasoner checks the consistency of $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases (KBs) represented in s…
▽ More
We present an ongoing implementation of a KE-tableau based reasoner for a decidable fragment of stratified elementary set theory expressing the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ (shortly $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$). The reasoner checks the consistency of $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-knowledge bases (KBs) represented in set-theoretic terms. It is implemented in \textsf{C++} and supports $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$-KBs serialized in the OWL/XML format. To the best of our knowledge, this is the first attempt to implement a reasoner for the consistency checking of a description logic represented via a fragment of set theory that can also classify standard OWL ontologies.
△ Less
Submitted 20 February, 2024; v1 submitted 21 July, 2017;
originally announced July 2017.
-
Speeding Up String Matching by Weak Factor Recognition
Authors:
Domenico Cantone,
Simone Faro,
Arianna Pavone
Abstract:
String matching is the problem of finding all the substrings of a text which match a given pattern. It is one of the most investigated problems in computer science, mainly due to its very diverse applications in several fields. Recently, much research in the string matching field has focused on the efficiency and flexibility of the searching procedure and quite effective techniques have been propo…
▽ More
String matching is the problem of finding all the substrings of a text which match a given pattern. It is one of the most investigated problems in computer science, mainly due to its very diverse applications in several fields. Recently, much research in the string matching field has focused on the efficiency and flexibility of the searching procedure and quite effective techniques have been proposed for speeding up the existing solutions. In this context, algorithms based on factors recognition are among the best solutions. In this paper, we present a simple and very efficient algorithm for string matching based on a weak factor recognition and hashing. Our algorithm has a quadratic worst-case running time. However, despite its quadratic complexity, experimental results show that our algorithm obtains in most cases the best running times when compared, under various conditions, against the most effective algorithms present in literature. In the case of small alphabets and long patterns, the gain in running times reaches 28%. This makes our proposed algorithm one of the most flexible solutions in practical cases.
△ Less
Submitted 3 July, 2017;
originally announced July 2017.
-
A set-theoretical approach for ABox reasoning services (Extended Version)
Authors:
Domenico Cantone,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
In this paper we consider the most common ABox reasoning services for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment \flqsr. The description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ is very e…
▽ More
In this paper we consider the most common ABox reasoning services for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment \flqsr. The description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ is very expressive, as it admits various concept and role constructs, and data types, that allow one to represent rule-based languages such as SWRL. Decidability results are achieved by defining a generalization of the conjunctive query answering problem, called HOCQA (Higher Order Conjunctive Query Answering), that can be instantiated to the most wide\-spread ABox reasoning tasks. We also present a \ke\space based procedure for calculating the answer set from $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ knowledge bases and higher order $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ conjunctive queries, thus providing means for reasoning on several well-known ABox reasoning tasks. Our calculus extends a previously introduced \ke\space based decision procedure for the CQA problem.
△ Less
Submitted 20 February, 2024; v1 submitted 10 February, 2017;
originally announced February 2017.
-
Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification
Authors:
Domenico Cantone,
Giorgio Delzanno
Abstract:
This volume contains the proceedings of the Seventh International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2016). The symposium took place in Catania, Italy, from the 14th to the 16th of September 2016. The proceedings of the symposium contain abstracts of the 3 invited talks and 21 full papers that were accepted after a careful evaluation for presentation at the confer…
▽ More
This volume contains the proceedings of the Seventh International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2016). The symposium took place in Catania, Italy, from the 14th to the 16th of September 2016. The proceedings of the symposium contain abstracts of the 3 invited talks and 21 full papers that were accepted after a careful evaluation for presentation at the conference. The topics of the accepted papers cover algorithmic game theory, automata theory, synthesis, formal verification, and dynamic, modal and temporal logics.
△ Less
Submitted 12 September, 2016;
originally announced September 2016.
-
Conjunctive Query Answering via a Fragment of Set Theory (Extended Version)
Authors:
Domenico Cantone,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
We address the problem of Conjunctive Query Answering (CQA) for the description logic $\dlssx$ ($\shdlssx$, for short) which extends the logic $\dlss$ with Boolean operations on concrete roles and with the product of concepts.
The result is obtained by formalizing $\shdlssx$-knowledge bases and $\shdlssx$-conjunctive queries in terms of formulae of the four-level set-theoretic fragment $\flqsr$,…
▽ More
We address the problem of Conjunctive Query Answering (CQA) for the description logic $\dlssx$ ($\shdlssx$, for short) which extends the logic $\dlss$ with Boolean operations on concrete roles and with the product of concepts.
The result is obtained by formalizing $\shdlssx$-knowledge bases and $\shdlssx$-conjunctive queries in terms of formulae of the four-level set-theoretic fragment $\flqsr$, which admits a restricted form of quantification on variables of the first three levels and on pair terms. We solve the CQA problem for $\shdlssx$ through a decision procedure for the satisfiability problem of $\flqsr$. We further define a \ke\space based procedure for the same problem, more suitable for implementation purposes, and analyze its computational complexity.
△ Less
Submitted 23 June, 2016;
originally announced June 2016.
-
The decision problem for a three-sorted fragment of set theory with restricted quantification and finite enumerations
Authors:
Domenico Cantone,
Marianna Nicolosi-Asmundo
Abstract:
We solve the satisfiability problem for a three-sorted fragment of set theory (denoted $3LQST_0^R$), which admits a restricted form of quantification over individual and set variables and the finite enumeration operator $\{\text{-}, \text{-}, \ldots, \text{-}\}$ over individual variables, by showing that it enjoys a small model property, i.e., any satisfiable formula $ψ$ of $3LQST_0^R$ has a finit…
▽ More
We solve the satisfiability problem for a three-sorted fragment of set theory (denoted $3LQST_0^R$), which admits a restricted form of quantification over individual and set variables and the finite enumeration operator $\{\text{-}, \text{-}, \ldots, \text{-}\}$ over individual variables, by showing that it enjoys a small model property, i.e., any satisfiable formula $ψ$ of $3LQST_0^R$ has a finite model whose size depends solely on the length of $ψ$ itself. Several set-theoretic constructs are expressible by $3LQST_0^R$-formulae, such as some variants of the power set operator and the unordered Cartesian product. In particular, concerning the unordered Cartesian product, we show that when finite enumerations are used to represent the construct, the resulting formula is exponentially shorter than the one that can be constructed without resorting to such terms.
△ Less
Submitted 4 June, 2015;
originally announced June 2015.
-
Web ontology representation and reasoning via fragments of set theory
Authors:
Domenico Cantone,
Cristiano Longo,
Marianna Nicolosi-Asmundo,
Daniele Francesco Santamaria
Abstract:
In this paper we use results from Computable Set Theory as a means to represent and reason about description logics and rule languages for the semantic web.
Specifically, we introduce the description logic $\mathcal{DL}\langle 4LQS^R\rangle(\D)$--admitting features such as min/max cardinality constructs on the left-hand/right-hand side of inclusion axioms, role chain axioms, and datatypes--which…
▽ More
In this paper we use results from Computable Set Theory as a means to represent and reason about description logics and rule languages for the semantic web.
Specifically, we introduce the description logic $\mathcal{DL}\langle 4LQS^R\rangle(\D)$--admitting features such as min/max cardinality constructs on the left-hand/right-hand side of inclusion axioms, role chain axioms, and datatypes--which turns out to be quite expressive if compared with $\mathcal{SROIQ}(\D)$, the description logic underpinning the Web Ontology Language OWL. Then we show that the consistency problem for $\mathcal{DL}\langle 4LQS^R\rangle(\D)$-knowledge bases is decidable by reducing it, through a suitable translation process, to the satisfiability problem of the stratified fragment $4LQS^R$ of set theory, involving variables of four sorts and a restricted form of quantification. We prove also that, under suitable not very restrictive constraints, the consistency problem for $\mathcal{DL}\langle 4LQS^R\rangle(\D)$-knowledge bases is \textbf{NP}-complete. Finally, we provide a $4LQS^R$-translation of rules belonging to the Semantic Web Rule Language (SWRL).
△ Less
Submitted 8 May, 2015;
originally announced May 2015.
-
NeatSort - A practical adaptive algorithm
Authors:
Marcello La Rocca,
Domenico Cantone
Abstract:
We present a new adaptive sorting algorithm which is optimal for most disorder metrics and, more important, has a simple and quick implementation. On input $X$, our algorithm has a theoretical $Ω(|X|)$ lower bound and a $\mathcal{O}(|X|\log|X|)$ upper bound, exhibiting amazing adaptive properties which makes it run closer to its lower bound as disorder (computed on different metrics) diminishes. F…
▽ More
We present a new adaptive sorting algorithm which is optimal for most disorder metrics and, more important, has a simple and quick implementation. On input $X$, our algorithm has a theoretical $Ω(|X|)$ lower bound and a $\mathcal{O}(|X|\log|X|)$ upper bound, exhibiting amazing adaptive properties which makes it run closer to its lower bound as disorder (computed on different metrics) diminishes. From a practical point of view, \textit{NeatSort} has proven itself competitive with (and often better than) \textit{qsort} and any \textit{Random Quicksort} implementation, even on random arrays.
△ Less
Submitted 23 July, 2014;
originally announced July 2014.
-
On the satisfiability problem for a 3-level quantified syllogistic
Authors:
Domenico Cantone,
Marianna Nicolosi Asmundo
Abstract:
We show that a collection of three-sorted set-theoretic formulae, denoted TLQSR and which admits a restricted form of quantification over individual and set variables, has a solvable satisfiability problem by proving that it enjoys a small model property, i.e., any satisfiable TLQSR-formula psi has a finite model whose size depends solely on the size of psi itself. We also introduce the sublanguag…
▽ More
We show that a collection of three-sorted set-theoretic formulae, denoted TLQSR and which admits a restricted form of quantification over individual and set variables, has a solvable satisfiability problem by proving that it enjoys a small model property, i.e., any satisfiable TLQSR-formula psi has a finite model whose size depends solely on the size of psi itself. We also introduce the sublanguages (TLQSR)^h of TLQSR, whose formulae are characterized by having quantifier prefixes of length bounded by h \geq 2 and some other syntactic constraints, and we prove that each of them has the satisfiability problem NP-complete. Then, we show that the modal logic S5 can be formalized in (TLQSR)^3.
△ Less
Submitted 8 April, 2013;
originally announced April 2013.
-
An Experiment on the Connection between the DLs' Family DL<ForAllPiZero> and the Real World
Authors:
Antonio Pisasale,
Domenico Cantone
Abstract:
This paper describes the analysis of a selected testbed of Semantic Web ontologies, by a SPARQL query, which determines those ontologies that can be related to the description logic DL<ForAllPiZero>, introduced in [4] and studied in [9]. We will see that a reasonable number of them is expressible within such computationally efficient language. We expect that, in a long-term view, a temporalization…
▽ More
This paper describes the analysis of a selected testbed of Semantic Web ontologies, by a SPARQL query, which determines those ontologies that can be related to the description logic DL<ForAllPiZero>, introduced in [4] and studied in [9]. We will see that a reasonable number of them is expressible within such computationally efficient language. We expect that, in a long-term view, a temporalization of description logics, and consequently, of OWL(2), can open new perspectives for the inclusion in this language of a greater number of ontologies of the testbed and, hopefully, of the "real world".
△ Less
Submitted 23 November, 2012; v1 submitted 21 November, 2012;
originally announced November 2012.
-
A decidable quantified fragment of set theory with ordered pairs and some undecidable extensions
Authors:
Domenico Cantone,
Cristiano Longo
Abstract:
In this paper we address the decision problem for a fragment of set theory with restricted quantification which extends the language studied in [4] with pair related quantifiers and constructs, in view of possible applications in the field of knowledge representation. We will also show that the decision problem for our language has a non-deterministic exponential time complexity. However, for the…
▽ More
In this paper we address the decision problem for a fragment of set theory with restricted quantification which extends the language studied in [4] with pair related quantifiers and constructs, in view of possible applications in the field of knowledge representation. We will also show that the decision problem for our language has a non-deterministic exponential time complexity. However, for the restricted case of formulae whose quantifier prefixes have length bounded by a constant, the decision problem becomes NP-complete. We also observe that in spite of such restriction, several useful set-theoretic constructs, mostly related to maps, are expressible. Finally, we present some undecidable extensions of our language, involving any of the operators domain, range, image, and map composition.
[4] Michael Breban, Alfredo Ferro, Eugenio G. Omodeo and Jacob T. Schwartz (1981): Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. Communications on Pure and Applied Mathematics 34, pp. 177-195
△ Less
Submitted 8 October, 2012;
originally announced October 2012.
-
On the satisfiability problem for a 4-level quantified syllogistic and some applications to modal logic (extended version)
Authors:
Domenico Cantone,
Marianna Nicolosi Asmundo
Abstract:
We introduce a multi-sorted stratified syllogistic, called 4LQSR, admitting variables of four sorts and a restricted form of quantification over variables of the first three sorts, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the fragments (4LQSR)^h of 4LQSR, consisting of 4LQSR-formulae whose quantifier prefixes have l…
▽ More
We introduce a multi-sorted stratified syllogistic, called 4LQSR, admitting variables of four sorts and a restricted form of quantification over variables of the first three sorts, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the fragments (4LQSR)^h of 4LQSR, consisting of 4LQSR-formulae whose quantifier prefixes have length bounded by h > 1 and satisfying certain syntactic constraints, and prove that each of them has an NP-complete satisfiability problem. Finally we show that the modal logic K45 can be expressed in 4LQSR^3.
△ Less
Submitted 10 September, 2012;
originally announced September 2012.
-
On Tuning the Bad-Character Rule: the Worst-Character Rule
Authors:
Domenico Cantone,
Simone Faro
Abstract:
In this note we present the worst-character rule, an efficient variation of the bad-character heuristic for the exact string matching problem, firstly introduced in the well-known Boyer-Moore algorithm. Our proposed rule selects a position relative to the current shift which yields the largest average advancement, according to the characters distribution in the text. Experimental results show that…
▽ More
In this note we present the worst-character rule, an efficient variation of the bad-character heuristic for the exact string matching problem, firstly introduced in the well-known Boyer-Moore algorithm. Our proposed rule selects a position relative to the current shift which yields the largest average advancement, according to the characters distribution in the text. Experimental results show that the worst-character rule achieves very good results especially in the case of long patterns or small alphabets in random texts and in the case of texts in natural languages.
△ Less
Submitted 6 December, 2010;
originally announced December 2010.
