Abstract The celebrated Ackermann encoding of hereditarily finite sets is generalized to a parametric formula designed to map not only these sets but also hereditarily finite multisets and hypersets into the non-negative real numbers. This extension suggests a novel approach to the graph canonization problem by reducing it to a simple comparison of real values. By suitably varying the sole parameter of this formula, both the original Ackermann encoding and another previously studied map emerge as special cases. When the parameter is chosen from the natural numbers, the function yields a bijective encoding of a subuniverse of hereditarily finite multisets into the natural numbers. If, instead, the parameter is chosen to be transcendental and lies within a specific interval on the positive real line, the function is conjectured to provide an injective encoding of both multisets and hypersets.

The Longest Common Substring (LCS) and Longest Palindromic Substring (LPS) problems are fundamental challenges in string processing, traditionally solved in linear time using classical computation through suffix trees. Recent breakthroughs by Le Gall and Seddighin [1] introduced sublinear quantum query algorithms, while Akmal and Jin [2] further improved the LCS complexity to O ˜ ( n 2 / 3 ) . While these results are remarkable in the quantum query model , their practical implementation on real quantum hardware remains elusive. In this paper, we bridge this gap by presenting the first O ˜ ( n ) quantum algorithms for both LCS and LPS in the circuit model of computation . Our circuits are explicitly constructed and analyzed in terms of size and depth, achieving polylogarithmic overheads while preserving the O ˜ ( n ) depth bound. This provides, for the first time, concrete circuit-level blueprints and resource estimates for quantum solutions to LCS and LPS.

We give a positive solution to the decidability problem for the fragment of set theory, dubbed BST ⊗, consisting of quantifier-free formulae involving the Boolean set operators of union, intersection, and set difference, along with the unordered Cartesian product operator ⊗ (where \(s \otimes t := \big \lbrace \lbrace u,v\rbrace \,\texttt {|}\:u \in s \wedge v \in t \big \rbrace\) ), and the equality predicate, but no membership. Specifically, we provide nondeterministic exponential decision procedures for both the ordinary and the finite satisfiability problems for BST ⊗. We expect that these decision procedures can be adapted for the standard Cartesian product and, with added technicalities, to the cases involving membership, providing a solution to a longstanding problem in computable set theory.

Abstract In a first-order theory $\varTheta $, the decision problem for a class of formulae $\varPhi $ is solvable if there is an algorithmic procedure that can assess whether or not the existential closure $\varphi ^{\exists }$ of $\varphi $ belongs to $\varTheta $, for any $\varphi \in \varPhi $. In 1988, Parlamento and Policriti already showed how to tailor arguments à la Gödel to a very weak axiomatic set theory, referring them to the class of $\varSigma _{1}$-formulae with $(\forall \exists \forall )_{0}$-matrix, i.e. existential closures of formulae that contain just restricted quantifiers of the forms $(\forall x \in y)$ and $(\exists x \in y)$ and are writable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a ‘$\forall $’). While revisiting their work, we show slightly less weak theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of $(\forall \exists )_{0}$-matrices, namely formulae with at most one alternation of restricted quantifiers.

We continue our investigation aimed at spotting small fragments of Set Theory (in this paper, sublanguages of Boolean Set Theory) that might be of use in automated proof-checkers based on the set-theoretic formalism. Here we propose a method that leads to a cubic-time satisfiability decision test for the language involving, besides variables intended to range over the von Neumann set-universe, the Boolean operator ∪ and the logical relators = and ≠. It can be seen that the dual language involving the Boolean operator ∩ and, again, the relators = and ≠, also admits a cubic-time satisfiability decision test; noticeably, the same algorithm can be used for both languages. Suitable pre-processing can reduce richer Boolean languages to the said two fragments, so that the same cubic satisfiability test can be used to treat the relators ⊆ and ⊈, and the predicates ‘’ and ‘’, meaning ‘the argument is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘’ and ‘’. Those richer languages are ‘polynomial maximal’, in the sense that each language strictly containing either of them and whose formulae are conjunctions of literals has an NP-hard satisfiability problem. A generalized version of the two said satisfiability tests can treat the relator ⊄, though at the price of a worsening of the algorithmic complexity (from cubic to quintic time).

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic 𝒟ℒ〈4LQSR,×〉(D) (𝒟ℒD4,×, for short). Our application solves the main TBox and ABox reasoning problems for 𝒟ℒD4,×. In particular, it solves the consistency and the classification problems for 𝒟ℒD4,×-knowledge bases represented in set-theoretic terms, and a generalization of the Conjunctive Query Answering problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and improves a previous version, is implemented in C++. It supports 𝒟ℒD4,×-knowledge bases serialized in the OWL/XML format and it admits also rules expressed in SWRL (Semantic Web Rule Language).

We report on an investigation aimed at identifying small fragments of set theory (typically, sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this paper we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪ ∩ \, the Boolean relators ⊆, ⊈,=, ≠, and the predicates ‘• = Ø’ and ‘Disj(•, •)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘• ≠ Ø and ‘¬Disj(•, •)’. We also examine in detail how to test for satisfiability the formulae of six sample fragments: three sample problems are shown to be NP-complete, two to admit quadratic-time decision algorithms, and one to be solvable in linear time.

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 approximate string matching problem when the edit operations are non-overlapping unbalanced translocations of adjacent factors. In particular, we first present a 𝒪(nm³)-time and 𝒪(m²)-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 𝒪(nlog²_{σ} m) average time complexity, for an alphabet of size σ, still maintaining the 𝒪(nm³)-time and the 𝒪(m²)-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.

In this paper we consider the most common TBox and ABox reasoning services for the description logic 𝒟ℒ〈4LQSR,x〉(D) ( 𝒟 ℒ D 4,× , for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment 4LQSR. 𝒟 ℒ D 4,× is a very expressive description logic. It combines the high scalability and efficiency of rule languages such as the SemanticWeb Rule Language (SWRL) with the expressivity of description logics. In fact, among other features, it supports 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, role properties such as transitivity, symmetry, reflexivity, and irreflexivity, and data types. We further provide a KE-tableau-based procedure that allows one to reason on the main TBox and ABox reasoning tasks for the description logic 𝒟 ℒ D 4,× . 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 [1] and of standard first-order KE-tableaux [2]. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that in several cases the performances of the KEγ-tableau-based reasoner are up to about 400% better than the ones of the other two systems.

In the last decades, several fragments of set theory have been studied in the context of Computable Set Theory. In general, the semantics of set-theoretic languages differs from the canonical first-order semantics in that the interpretation domain of set-theoretic terms is fixed to a given universe of sets. Because of this, theoretical results and various machinery developed in the context of first-order logic could be not easily applicable in the set-theoretic realm. Recently, the decidability of quantified fragments of set theory which allow one to explicitly handle ordered pairs has been studied, in view of applications in the field of knowledge representation. Among other results, a NEXPTIME decision procedure for satisfiability of formulae in one of these fragments, ∀0π , has been devised. In this paper we exploit the main features of such a decision procedure to reduce the satisfiability problem for the fragment ∀0π to the problem of Herbrand satisfiability for a first-order language extending it. In addition, it turns out that such a reduction maps formulae of the Disjunctive Datalog subset of ∀0π into Disjunctive Datalog formulae.

We introduce a multi-sorted stratified syllogistic, called 4LQS R , 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 (4LQS R ) h of 4LQS R , consisting of 4LQS R -formulae whose quantifier prefixes have length bounded by h ≥ 2 and satisfying certain additional syntactical 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 (4LQS R ) 3 .

Range and k-nearest neighbor searching are core problems in pattern recognition. Given a database S of objects in a metric space M and a query object q in M, in a range searching problem the goal is to find the objects of S within some threshold distance to g, whereas in a k-nearest neighbor searching problem, the k elements of S closest to q must be produced. These problems can obviously be solved with a linear number of distance calculations, by comparing the query object against every object in the database. However, the goal is to solve such problems much faster. We combine and extend ideas from the M-tree, the multivantage point structure, and the FQ-tree to create a new structure in the "bisector tree" class, called the Antipole tree. Bisection is based on the proximity to an "Antipole" pair of elements generated by a suitable linear randomized tournament. The final winners a, b of such a tournament is far enough apart to approximate the diameter of the splitting set. If dist(a, b) is larger than the chosen cluster diameter threshold, then the cluster is split. The proposed data structure is an indexing scheme suitable for (exact and approximate) best match searching on generic metric spaces. The Antipole tree outperforms by a factor of approximately two existing structures such as list of clusters, M-trees, and others and, in many cases, it achieves better clustering properties.

In this paper we show that a class of unquantified multisorted set-theoretic formulae involving the notions of powerset, general union, and singleton has a solvable satisfiability problem.We show by means of a model normalization procedure that any given satisfiable formula in our theory has a finite model whose size is bounded by a function of the number of variables occurring in it.

The class of purely universal formulae of the elementary theory of relations with equality is shown to have an NP-complete satisfiability problem, under the assumption that there is an a priori bound on the length of quantifier prefixes and the arities of relation variables. In the second part of the paper we discuss possible applications in the field of theorem proving in set and graph theory and of consistency checking for queries in relational databases.

“Boole first put forth the problem of Logical Science in its complete generality: Given certain logical premisses or conditions, to determine the description of any class of objects under those conditions .”

Etude des procedures de decision pour differents sous-langages restreints quantifies et non quantifies de la theorie des ensembles