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.

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 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.

The Italian Conference on Computational Logic -CILC-is the annual conference organized by GULP (Group of researchers and Users of Logic Programming).Since the first event of the series, which took place in Genoa in 1986, the annual GULP conference represents the main opportunity for Italian users, researchers and developers working in the field of computational logic to meet and exchange ideas.Over the years the conference broadened its horizons from the specific field of logic programming to include declarative programming and applications in neighboring areas such as artificial intelligence and deductive databases.This special issue contains revised and extended versions of papers presented at the 34th Italian Conference on Computational Logic -CILC 2019-which was hosted by the University of Trieste, Italy, from June 19 to June 21, 2019.The authors of selected papers were invited to submit an improved, extended version to this special issue of Fundamenta Informaticae.Those papers went through a careful review by qualified international referees.The three papers in the special issue witness the multifaceted nature of CILC, covering important topics in formal verification, automated theorem proving, and knowledge representation.We would like to thank the Editorial Office of Fundamenta Informaticae, and in particular the Editor-in-Chief Damian Niwiński.Finally, we thank the authors of the papers

This paper considers ∃*∀* prenex sentences of pure first-order predicate calculus with equality. This is the set of formulas which Ramsey's treated in a famous article of 1930. We demonstrate that the satisfiability problem and the problem of existence of arbitrarily large models for these formulas can be reduced to the satisfiability problem for ∃*∀* prenex sentences of Set Theory (in the relators ∈, =). We present two satisfiability-preserving (in a broad sense) translations Φ ↦ $\dot{\Phi}$ and Φ ↦ Φσ of ∃*∀* sentences from pure logic to well-founded Set Theory, so that if $\dot{\Phi}$ is satisfiable (in the domain of Set Theory) then so is Φ, and if Φσ is satisfiable (again, in the domain of Set Theory) then Φ can be satisfied in arbitrarily large finite structures of pure logic. It turns out that | $\dot{\Phi}$ | = $\mathcal{O}$ (|Φ|) and |Φσ| = $\mathcal{O}$ (|Φ|2). Our main result makes use of the fact that ∃*∀* sentences, even though constituting a decidable fragment of Set Theory, offer ways to describe infinite sets. Such a possibility is exploited to glue together infinitely many models of increasing cardinalities of a given ∃*∀* logical formula, within a single pair of infinite sets.

We introduce and prove the basic properties of encodings that generalize to non-well-founded hereditarily finite sets the bijection defined by Ackermann in 1937 between hereditarily finite sets and natural numbers.

An undirected graph is commonly represented as a set of vertices and a set of vertex doubletons; but one can also represent each vertex by a finite set so as to ensure that membership mimics, over these vertex-representing sets, the edge relation of the graph. This alternative modelling, applied to connected claw-free graphs, recently gave crucial clues for obtaining simpler proofs of some of their properties (e.g. Hamiltonicity of the square of the graph). This article adds a computer-checked contribution. On the one hand, we discuss our development, by means of the Ref verifier, of two theorems on representing graphs by families of finite sets: a weaker theorem pertains to general graphs, and a stronger one to connected claw-free graphs. Before proving those theorems, we must show that every graph admits an acyclic, weakly extensional orientation, which becomes fully extensional when connectivity and claw-freeness are met. This preliminary work enables injective decoration, à la Mostowski, of the vertices by the sought-for finite sets. By this new scenario, we complement our earlier formalization with Ref of two classical properties of connected claw-free graphs. On the other hand, our present work provides another example of the ease with which graph-theoretic results are proved with the Ref verifier. For example, we managed to define and exploit the notion of connected graph without resorting to the notion of path.

Abstract As proved recently, the satisfaction problem for all prenex formulae in the set-theoretic Bernays-Shönfinkel-Ramsey class is semi-decidable over von Neumann's cumulative hierarchy. Here that semi-decidability result is strengthened into a decidability result for the same collection of formulae.

It is shown that within the language of Set Theory, if membership is assumed to be non-well-founded à la Aczel, then one can state the existence of infinite sets by means of an ∃∃∀∀ prenex sentence. Somewhat surprisingly, this statement of infinity is essentially the one which was proposed in 1988 for well-founded sets, and it is satisfied exclusively by well-founded sets. Stating infinity inside the BSR (Bernays–Schönfinkel–Ramsey) class of the ∃*∀*-sentences becomes more challenging if no commitment is taken as whether membership is well-founded or not: for this case, we produce an ∃∃∀∀∀ -sentence, thus lowering the complexity of the quantificational prefix with respect to earlier prenex formulations of infinity. We also show that no prenex specification of infinity can have a prefix simpler than ∃∃∀∀. The problem of determining whether a BSR-sentence involving an uninterpreted predicate symbol and = can be satisfied over a large domain is then reduced to the satisfiability problem for the set theoretic class BSR subject to the ill-foundedness assumption. Envisaged enhancements of this reduction, cleverly exploiting the expressive power of the set theoretic BSR-class, add to the motivation for tackling the satisfaction problem for this class, which appears to be anything but unchallenging.

Abstract As is well-known, the Bernays-Schönfinkel-Ramsey class of all prenex ∃*∀*-sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are ∈ and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach, the remaining part of the decidability result being postponed to a forthcoming paper.

Formal set theory is traditionally concerned with pure sets; consequently, the satisfiability problem for fragments of set theory was most often addressed (and in many cases positively solved) in the pure framework. In practical applications, however, it is common to assume the existence of a number of primitive objects (sometimes called atoms ) that can be members of sets but behave differently from them. If these entities are assumed to be devoid of members, the standard extensionality axiom must be revised; then decidability results can sometimes be achieved via reduction to the pure case and sometimes can be based on direct goal-driven algorithms. An alternative approach to modeling atoms that allows one to retain the original formulation of extensionality was proposed by Quine: atoms are self-singletons. In this article we adopt this approach in coping with the satisfiability problem: We show the decidability of this problem relativized to ∃*∀-sentences, and develop a goal-driven unification algorithm.

Abstract Being able to state the principles which lie deepest in the foundations of mathematics by sentences in three variables is crucially important for a satisfactory equational rendering of set theories along the lines proposed by Alfred Tarski and Steven Givant in their monograph of 1987. The main achievement of this paper is the proof that the ‘kernel’ set theory whose postulates are extensionality. (E), and single-element adjunction and removal. (W) and (L), cannot be axiomatized by means of three-variable sentences. This highlights a sharp edge to be crossed in order to attain an ‘algebraization’ of Set Theory. Indeed, one easily shows that the theory which results from the said kernel by addition of the null set axiom, (N), is in its entirety expressible in three variables.

“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 .”