Tharindu Madusanka, Marco Valentino, Iqra Zahid, Ian Pratt-Hartmann, Riza Batista-Navarro. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2025.

Abstract We introduce the adjacent fragment $\mathcal{AF}$ of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) the two-variable fragment of first-order logic as well as the so-called fluted fragment. We show that the adjacent fragment has the finite model property, and that the satisfiability problem for its $k$-variable sub-fragment is in $(k{-}1)$-$\text{NExpTime}$. Using known results on the fluted fragment, it follows that the satisfiability problem for the whole adjacent fragment is $\text{Tower}$-complete. We additionally consider the effect of the adjacency requirement on the well-known guarded fragment of first-order logic, whose satisfiability problem is $2\text{ExpTime}$-complete. We show that the satisfiability problem for the intersection of the adjacent and guarded adjacent fragments remains $2\text{ExpTime}$-hard. Finally, we show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable.

Efforts to apply transformer-based language models (TLMs) to the problem of reasoning in natural language have enjoyed ever-increasing success in recent years.The most fundamental task in this area to which nearly all others can be reduced is that of determining satisfiability.However, from a logical point of view, satisfiability problems vary along various dimensions, which may affect TLMs' ability to learn how to solve them.The problem instances of satisfiability in natural language can belong to different computational complexity classes depending on the language fragment in which they are expressed.Although prior research has explored the problem of natural language satisfiability, the above-mentioned point has not been discussed adequately.Hence, we investigate how problem instances from varying computational complexity classes and having different grammatical constructs impact TLMs' ability to learn rules of inference.Furthermore, to faithfully evaluate TLMs, we conduct an empirical study to explore the distribution of satisfiability problems.

Any function f with domain {1, … , m} and co-domain {1, … , n} induces a natural map from words of length n to those of length m: the ith letter of the output word (1 ≤ i ≤ m) is given by the f(i)th letter of the input word. We study this map in the case where f is a surjection satisfying the condition |f(i+1)-f(i)| ≤ 1 for 1 ≤ i < m. Intuitively, we think of f as describing a "walk" on a word u, visiting every position, and yielding a word w as the sequence of letters encountered en route. If such an f exists, we say that u generates w. Call a word primitive if it is not generated by any word shorter than itself. We show that every word has, up to reversal, a unique primitive generator. Observing that, if a word contains a non-trivial palindrome, it can generate the same word via essentially different walks, we obtain conditions under which, for a chosen pair of walks f and g, those walks yield the same word when applied to a given primitive word. Although the original impulse for studying primitive generators comes from their application to decision procedures in logic, we end, by way of further motivation, with an analysis of the primitive generators for certain word sequences defined via morphisms.

Can transformers learn to comprehend logical semantics in natural language?Although many strands of work on natural language inference have focussed on transformer models' ability to perform reasoning on text, the above question has not been answered adequately.This is primarily because the logical problems that have been studied in the context of natural language inference have their computational complexity vary with the logical and grammatical constructs within the sentences.As such, it is difficult to access whether the difference in accuracy is due to logical semantics or the difference in computational complexity.A problem that is much suited to address this issue is that of the model-checking problem, whose computational complexity remains constant (for fragments derived from first-order logic).However, the model-checking problem remains untouched in natural language inference research.Thus, we investigated the problem of model-checking with natural language to adequately answer the question of how the logical semantics of natural language affects transformers' performance 1 .Our results imply that the language fragment has a significant impact on the performance of transformer models.Furthermore, we hypothesise that a transformer model can at least partially understand the logical semantics in natural language but can not completely learn the rules governing the modelchecking algorithm.

How do different generalised quantifiers affect the behaviour of transformer-based language models (TLMs)?The recent popularity of TLMs and the central role generalised quantifiers have traditionally played in linguistics and logic bring this question into particular focus.The current research investigating this subject has not utilised a task defined purely in a logical sense, and thus, has not captured the underlying logical significance of generalised quantifiers.Consequently, they have not answered the aforementioned question faithfully or adequately.Therefore, we investigate how different generalised quantifiers affect TLMs by employing a textual entailment problem defined in a purely logical sense, namely, modelchecking with natural language.Our approach permits the automatic construction of datasets with respect to which we can assess the ability of TLMs to learn the meanings of generalised quantifiers.Our investigation reveals that TLMs generally can comprehend the logical semantics of the most common generalised quantifiers, but that distinct quantifiers influence TLMs in varying ways.

We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.

State-of-the-artdeep-learning-based approaches to Natural Language Processing (NLP) are credited with various capabilities that involve reasoning with natural language texts.In this paper we carry out a large-scale empirical study investigating the detection of formally valid inferences in controlled fragments of natural language for which the satisfiability problem becomes increasingly complex.We find that, while transformerbased language models perform surprisingly well in these scenarios, a deeper analysis reveals that they appear to overfit to superficial patterns in the data rather than acquiring the logical principles governing the reasoning in these fragments.

The fluted fragment is a fragment of first-order logic in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that the fluted fragment possesses the finite model property. In this paper, we extend the fluted fragment by the addition of counting quantifiers. We show that the resulting logic retains the finite model property, and that the satisfiability problem for its (m+1)-variable sub-fragment is in m-NExpTime for all positive m. We also consider the satisfiability and finite satisfiability problems for the extension of any of these fragments in which the fluting requirement applies only to sub-formulas having at least three free variables.

We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

Abstract We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$ , the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all $m \ge 1$ . We show that, for $m \ge 2$ , this subfragment forces $\left\lfloor {m/2} \right\rfloor$ -tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$ -NExpTime-hard. We further establish that, for $m \ge 3$ , any satisfiable ${\cal F}{{\cal L}^m}$ -formula has a model of at most ( $m - 2$ )-tuply exponential size, whence the satisfiability (= finite satisfiability) problem for this fragment is in ( $m - 2$ )-NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for ${\cal F}{{\cal L}^m}$ for all $m \le 4$ .

We consider an extension of two-variable, first-order logic with counting quantifiers and arbitrarily many unary and binary predicates, in which one distinguished predicate is interpreted as the mother-daughter relation in an unranked forest. We show that both the finite satisfiability and the general satisfiability problems for the extended logic are decidable in NExpTime. We also show that the decision procedure for finite satisfiability can be extended to the logic where two distinguished predicates are interpreted as the mother-daughter relations in two independent forests.

The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.

We consider the satisfiability and finite satisfiability problems for the extension of the two-variable guarded fragment in which an equivalence closure operator can be applied to two distinguished binary predicates.We show that the satisfiability and finite satisfiability problems for this logic are 2-ExpTime-complete.This contrasts with an earlier result that the corresponding problems for the full two-variable logic with equivalence closures of two binary predicates are 2-NExpTime-complete.

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified by W.V. Quine. We show that the satisfiability problem for this fragment has non-elementary complexity, thus refuting an earlier published claim by W.C. Purdy that it is in NExpTime. More precisely, we consider, for all m greater than 1, the intersection of the fluted fragment and the m-variable fragment of first-order logic. We show that this sub-fragment forces (m/2)-tuply exponentially large models, and that its satisfiability problem is (m/2)-NExpTime-hard. We round off by using a corrected version of Purdy's construction to show that the m-variable fluted fragment has the m-tuply exponential model property, and that its satisfiability problem is in m-NExpTime.

We consider the satisfiability and finite satisfiability problems for extensions of the two-variable fragment of first-order logic in which an equivalence closure operator can be applied to a fixed number of binary predicates. We show that the satisfiability problem for two-variable, first-order logic with equivalence closure applied to two binary predicates is in 2-NExpTime, and we obtain a matching lower bound by showing that the satisfiability problem for two-variable first-order logic in the presence of two equivalence relations is 2-NExpTime-hard. The logics in question lack the finite model property; however, we show that the same complexity bounds hold for the corresponding finite satisfiability problems. We further show that the satisfiability (${=}$ finite satisfiability) problem for the two-variable fragment of first-order logic with equivalence closure applied to a single binary predicate is NExpTime-complete.

A "numerical set-expression" is a term specifying a cascade of arithmetic and logical operations to be performed on sets of non-negative integers. If these operations are confined to the usual Boolean operations together with the result of lifting addition to the level of sets, we speak of "additive circuits". If they are confined to the usual Boolean operations together with the result of lifting addition and multiplication to the level of sets, we speak of "arithmetic circuits". In this paper, we investigate the definability of sets and functions by means of additive and arithmetic circuits, occasionally augmented with additional operations.

We consider the quantifier-free languages, Bc and Bc °, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of R n ( n ≥ 2) and, additionally, over the regular closed semilinear sets of R n . The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric Qualitative Spatial Reasoning. We prove that the satisfiability problem for Bc is undecidable over the regular closed semilinear sets in all dimensions greater than 1, and that the satisfiability problem for Bc and Bc ° is undecidable over both the regular closed sets and the regular closed semilinear sets in the Euclidean plane. However, we also prove that the satisfiability problem for Bc ° is NP-complete over the regular closed sets in all dimensions greater than 2, while the corresponding problem for the regular closed semilinear sets is ExpTime -complete. Our results show, in particular, that spatial reasoning is much harder over Euclidean spaces than over arbitrary topological spaces.

We consider the satisfiability and finite satisfiability problems for extensions of the two-variable fragment of first-order logic in which an equivalence closure operator can be applied to a fixed number of binary predicates. We show that the satisfiability problem for two-variable, first-order logic with equivalence closure applied to two binary predicates is in 2NEXPTIME, and we obtain a matching lower bound by showing that the satisfiability problem for two-variable first-order logic in the presence of two equivalence relations is 2NEXPTIME-hard. The logics in question lack the finite model property; however, we show that the same complexity bounds hold for the corresponding finite satisfiability problems. We further show that the satisfiability (=finite satisfiability) problem for the two-variable fragment of first-order logic with equivalence closure applied to a single binary predicate is NEXPTIME-complete.

We investigate (quantifier-free) spatial constraint languages with equality, contact and connectedness predicates, as well as Boolean operations on regions, interpreted over low-dimensional Euclidean spaces. We show that the complexity of reasoning varies dramatically depending on the dimension of the space and on the type of regions considered. For example, the logic with the interior-connectedness predicate (and without contact) is undecidable over polygons or regular closed sets in ℝ2, EXPTIME-complete over polyhedra in ℝ3, and NP-complete over regular closed sets in ℝ3.

An interval temporal logic is a propositional, multi-modal logic interpreted over interval structures of partial orders. The semantics of each modal operator are given in the standard way with respect to one of the natural accessibility relations defined on such interval structures. In this paper, we consider the modal operators based on the (reflexive) sub-interval relation and the (reflexive) super-interval relation. We show that the satisfiability problems for the interval temporal logics featuring either or both of these modalities, interpreted over interval structures of finite linear orders, are all PSPACE-complete. These results fill a gap in the known complexity results for interval temporal logics.

Graded modal logic is the formal language obtained from ordinary modal logic by endowing its modal operators with cardinality constraints. Under the familiar possible-worlds semantics, these augmented modal operators receive interpretations such as "It is true at no fewer than 15 accessible worlds that ...", or "It is true at no more than 2 accessible worlds that ...". We investigate the complexity of satisfiability for this language over some familiar classes of frames. This problem is more challenging than its ordinary modal logic counterpart-especially in the case of transitive frames, where graded modal logic lacks the tree-model property. We obtain tight complexity bounds for the problem of determining the satisfiability of a given graded modal logic formula over the classes of frames characterized by any combination of reflexivity, seriality, symmetry, transitivity and the Euclidean property.

An arithmetic circuit is a labeled, acyclic directed graph specifying a sequence of arithmetic and logical operations to be performed on sets of natural numbers. Arithmetic circuits can also be viewed as the elements of the smallest subalgebra of the complex algebra of the semiring of natural numbers. In the present paper we investigate the algebraic structure of complex algebras of natural numbers and make some observations regarding the complexity of various theories of such algebras.

The finite satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME.

This extended abstract reports on the computational complexity of reasoning with English sentences featuring temporal prepositions. A fragment of English featuring these constructions, called TPE, is defined by means of a context-free grammar. The phrase-structures which this grammar assigns to the sentences it recognizes can be viewed as formulas of an interval temporal logic, called TPL, whose satisfaction-conditions faithfully represent the meanings of the corresponding English sentences. It is shown that the satisfiability problem for TPL is NEXPTIME-complete.

Abstract In recent years, there has been renewed interest in the development of formal languages for describing mereological (part-whole) and topological relationships between objects in space. Typically, the non-logical primitives of these languages are properties and relations such as ‘xis connected’ or ‘xis a part ofy’, and the entities over which their variables range are, accordingly, notpoints, butregions: spatial entities other than regions are admitted, if at all, only as logical constructs of regions. This paper considers two first-order mereotopological languages, and investigates their expressive power. It turns out that these languages, notwithstanding the simplicity of their primitives, are surprisingly expressive. In particular, it is shown that infinitary versions of these languages are adequate to express (in a sense made precise below) all topological relations over the domain of polygons in the closed plane.