Showing 1–27 of 27 results for author: Pratt-Hartmann, I

Improving Semantic Control in Discrete Latent Spaces with Transformer Quantized Variational Autoencoders

Authors: Yingji Zhang, Danilo S. Carvalho, Marco Valentino, Ian Pratt-Hartmann, Andre Freitas

Abstract: Achieving precise semantic control over the latent spaces of Variational AutoEncoders (VAEs) holds significant value for downstream tasks in NLP as the underlying generative mechanisms could be better localised, explained and improved upon. Recent research, however, has struggled to achieve consistent results, primarily due to the inevitable loss of semantic information in the variational bottlene… ▽ More Achieving precise semantic control over the latent spaces of Variational AutoEncoders (VAEs) holds significant value for downstream tasks in NLP as the underlying generative mechanisms could be better localised, explained and improved upon. Recent research, however, has struggled to achieve consistent results, primarily due to the inevitable loss of semantic information in the variational bottleneck and limited control over the decoding mechanism. To overcome these challenges, we investigate discrete latent spaces in Vector Quantized Variational AutoEncoders (VQVAEs) to improve semantic control and generation in Transformer-based VAEs. In particular, We propose T5VQVAE, a novel model that leverages the controllability of VQVAEs to guide the self-attention mechanism in T5 at the token-level, exploiting its full generalization capabilities. Experimental results indicate that T5VQVAE outperforms existing state-of-the-art VAE models, including Optimus, in terms of controllability and preservation of semantic information across different tasks such as auto-encoding of sentences and mathematical expressions, text transfer, and inference. Moreover, T5VQVAE exhibits improved inference capabilities, suggesting potential applications for downstream natural language and symbolic reasoning tasks. △ Less

Submitted 1 February, 2024; originally announced February 2024.

LlaMaVAE: Guiding Large Language Model Generation via Continuous Latent Sentence Spaces

Authors: Yingji Zhang, Danilo S. Carvalho, Ian Pratt-Hartmann, André Freitas

Abstract: Deep generative neural networks, such as Variational AutoEncoders (VAEs), offer an opportunity to better understand and control language models from the perspective of sentence-level latent spaces. To combine the controllability of VAE latent spaces with the state-of-the-art performance of recent large language models (LLMs), we present in this work LlaMaVAE, which combines expressive encoder and… ▽ More Deep generative neural networks, such as Variational AutoEncoders (VAEs), offer an opportunity to better understand and control language models from the perspective of sentence-level latent spaces. To combine the controllability of VAE latent spaces with the state-of-the-art performance of recent large language models (LLMs), we present in this work LlaMaVAE, which combines expressive encoder and decoder models (sentenceT5 and LlaMA) with a VAE architecture, aiming to provide better text generation control to LLMs. In addition, to conditionally guide the VAE generation, we investigate a new approach based on flow-based invertible neural networks (INNs) named Invertible CVAE. Experimental results reveal that LlaMaVAE can outperform the previous state-of-the-art VAE language model, Optimus, across various tasks, including language modelling, semantic textual similarity and definition modelling. Qualitative analysis on interpolation and traversal experiments also indicates an increased degree of semantic clustering and geometric consistency, which enables better generation control. △ Less

Submitted 20 December, 2023; originally announced December 2023.

Graph-Induced Syntactic-Semantic Spaces in Transformer-Based Variational AutoEncoders

Authors: Yingji Zhang, Marco Valentino, Danilo S. Carvalho, Ian Pratt-Hartmann, André Freitas

Abstract: The injection of syntactic information in Variational AutoEncoders (VAEs) has been shown to result in an overall improvement of performances and generalisation. An effective strategy to achieve such a goal is to separate the encoding of distributional semantic features and syntactic structures into heterogeneous latent spaces via multi-task learning or dual encoder architectures. However, existing… ▽ More The injection of syntactic information in Variational AutoEncoders (VAEs) has been shown to result in an overall improvement of performances and generalisation. An effective strategy to achieve such a goal is to separate the encoding of distributional semantic features and syntactic structures into heterogeneous latent spaces via multi-task learning or dual encoder architectures. However, existing works employing such techniques are limited to LSTM-based VAEs. In this paper, we investigate latent space separation methods for structural syntactic injection in Transformer-based VAE architectures (i.e., Optimus). Specifically, we explore how syntactic structures can be leveraged in the encoding stage through the integration of graph-based and sequential models, and how multiple, specialised latent representations can be injected into the decoder's attention mechanism via low-rank operators. Our empirical evaluation, carried out on natural language sentences and mathematical expressions, reveals that the proposed end-to-end VAE architecture can result in a better overall organisation of the latent space, alleviating the information loss occurring in standard VAE setups, resulting in enhanced performances on language modelling and downstream generation tasks. △ Less

Submitted 14 November, 2023; originally announced November 2023.

Towards Controllable Natural Language Inference through Lexical Inference Types

Authors: Yingji Zhang, Danilo S. Carvalho, Ian Pratt-Hartmann, Andre Freitas

Abstract: Explainable natural language inference aims to provide a mechanism to produce explanatory (abductive) inference chains which ground claims to their supporting premises. A recent corpus called EntailmentBank strives to advance this task by explaining the answer to a question using an entailment tree \cite{dalvi2021explaining}. They employ the T5 model to directly generate the tree, which can explai… ▽ More Explainable natural language inference aims to provide a mechanism to produce explanatory (abductive) inference chains which ground claims to their supporting premises. A recent corpus called EntailmentBank strives to advance this task by explaining the answer to a question using an entailment tree \cite{dalvi2021explaining}. They employ the T5 model to directly generate the tree, which can explain how the answer is inferred. However, it lacks the ability to explain and control the generation of intermediate steps, which is crucial for the multi-hop inference process. % One recent corpus, EntailmentBank, aims to push this task forward by explaining an answer to a question according to an entailment tree \cite{dalvi2021explaining}. They employ T5 to generate the tree directly, which can explain how the answer is inferred but cannot explain how the intermediate is generated, which is essential to the multi-hop inference process. In this work, we focus on proposing a controlled natural language inference architecture for multi-premise explanatory inference. To improve control and enable explanatory analysis over the generation, we define lexical inference types based on Abstract Meaning Representation (AMR) graph and modify the architecture of T5 to learn a latent sentence representation (T5 bottleneck) conditioned on said type information. We also deliver a dataset of approximately 5000 annotated explanatory inference steps, with well-grounded lexical-symbolic operations. Experimental results indicate that the inference ty** induced at the T5 bottleneck can help T5 to generate a conclusion under explicit control. △ Less

Submitted 7 August, 2023; originally announced August 2023.

On the Limits of Decision: the Adjacent Fragment of First-Order Logic

Authors: Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann

Abstract: 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 fr… ▽ More 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. △ Less

Submitted 15 June, 2023; v1 submitted 4 May, 2023; originally announced May 2023.

Comments: Full version of our ICALP 2023 paper

Can Transformers Reason in Fragments of Natural Language?

Authors: Viktor Schlegel, Kamen V. Pavlov, Ian Pratt-Hartmann

Abstract: State-of-the-art deep-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.… ▽ More State-of-the-art deep-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 transformer-based language models perform surprisingly well in these scenarios, a deeper analysis re-veals that they appear to overfit to superficial patterns in the data rather than acquiring the logical principles governing the reasoning in these fragments. △ Less

Submitted 10 November, 2022; originally announced November 2022.

Comments: Accepted to EMNLP 2022

Formal Semantic Geometry over Transformer-based Variational AutoEncoder

Authors: Yingji Zhang, Danilo S. Carvalho, Ian Pratt-Hartmann, André Freitas

Abstract: Formal/symbolic semantics can provide canonical, rigid controllability and interpretability to sentence representations due to their \textit{localisation} or \textit{composition} property. How can we deliver such property to the current distributional sentence representations to control and interpret the generation of language models (LMs)? In this work, we theoretically frame the sentence semanti… ▽ More Formal/symbolic semantics can provide canonical, rigid controllability and interpretability to sentence representations due to their \textit{localisation} or \textit{composition} property. How can we deliver such property to the current distributional sentence representations to control and interpret the generation of language models (LMs)? In this work, we theoretically frame the sentence semantics as the composition of \textit{semantic role - word content} features and propose the formal semantic geometry. To inject such geometry into Transformer-based LMs (i.e. GPT2), we deploy Transformer-based Variational AutoEncoder with a supervision approach, where the sentence generation can be manipulated and explained over low-dimensional latent Gaussian space. In addition, we propose a new probing algorithm to guide the movement of sentence vectors over such geometry. Experimental results reveal that the formal semantic geometry can potentially deliver better control and interpretation to sentence generation. △ Less

Submitted 11 June, 2024; v1 submitted 12 October, 2022; originally announced October 2022.

Walking on Words

Authors: Ian Pratt-Hartmann

Abstract: Take any word over some alphabet. If it is non-empty, go to any position and print out the letter being scanned. Now repeat the following any number of times (possibly zero): either stay at the current letter, or move one letter leftwards (if possible) or move one letter rightwards (if possible); then print out the letter being scanned. In effect, we are going for a walk on the input word. Let u b… ▽ More Take any word over some alphabet. If it is non-empty, go to any position and print out the letter being scanned. Now repeat the following any number of times (possibly zero): either stay at the current letter, or move one letter leftwards (if possible) or move one letter rightwards (if possible); then print out the letter being scanned. In effect, we are going for a walk on the input word. Let u be the infix of the input word comprising the visited positions, and w the word printed out (empty if the input word is). Since any unvisited prefix or suffix of the input word cannot influence w, we may as well discard them, and say that u generates w. We ask: given a word w, what words u generate it? The answer is surprising. Call u a primitive generator of w if u generates w and is not generated by any word shorter than u. We show that, excepting some degenerate cases, every word has precisely two primitive generators. △ Less

Submitted 20 April, 2024; v1 submitted 18 August, 2022; originally announced August 2022.

Comments: Considerably extended from v1. (Secs. 4, 5 and 6 added.)

MSC Class: 68Q42 ACM Class: F.4.2; G.2.1

Do Natural Language Explanations Represent Valid Logical Arguments? Verifying Entailment in Explainable NLI Gold Standards

Authors: Marco Valentino, Ian Pratt-Hartmann, André Freitas

Abstract: An emerging line of research in Explainable NLP is the creation of datasets enriched with human-annotated explanations and rationales, used to build and evaluate models with step-wise inference and explanation generation capabilities. While human-annotated explanations are used as ground-truth for the inference, there is a lack of systematic assessment of their consistency and rigour. In an attemp… ▽ More An emerging line of research in Explainable NLP is the creation of datasets enriched with human-annotated explanations and rationales, used to build and evaluate models with step-wise inference and explanation generation capabilities. While human-annotated explanations are used as ground-truth for the inference, there is a lack of systematic assessment of their consistency and rigour. In an attempt to provide a critical quality assessment of Explanation Gold Standards (XGSs) for NLI, we propose a systematic annotation methodology, named Explanation Entailment Verification (EEV), to quantify the logical validity of human-annotated explanations. The application of EEV on three mainstream datasets reveals the surprising conclusion that a majority of the explanations, while appearing coherent on the surface, represent logically invalid arguments, ranging from being incomplete to containing clearly identifiable logical errors. This conclusion confirms that the inferential properties of explanations are still poorly formalised and understood, and that additional work on this line of research is necessary to improve the way Explanation Gold Standards are constructed. △ Less

Submitted 15 May, 2021; v1 submitted 5 May, 2021; originally announced May 2021.

Comments: To appear in IWCS 2021 proceedings

The Fluted Fragment with Transitive Relations

Authors: Ian Pratt-Hartmann, Lidia Tendera

Abstract: We study the satisfiability problem for the fluted fragment extended with transitive relations. The logic enjoys the finite model property when only one transitive relation is available and the finite model property is lost when additionally either equality or a second transitive relation is allowed. We show that the satisfiability problem for the fluted fragment with one transitive relation and e… ▽ More We study the satisfiability problem for the fluted fragment extended with transitive relations. The logic enjoys the finite model property when only one transitive relation is available and the finite model property is lost when additionally either equality or a second transitive relation is allowed. We show that the satisfiability problem for the fluted fragment with one transitive relation and equality remains decidable. 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 (or two transitive relations and equality). △ Less

Submitted 19 June, 2020; originally announced June 2020.

MSC Class: 03D15 ACM Class: F.4.1; F.2.2

Journal ref: Annals of Pure and Applied Logic 173, 2022, art. 103042, pp. 1--43

The Fluted Fragment with Transitivity

Authors: Ian Pratt-Hartmann, Lidia Tendera

Abstract: 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. 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. △ Less

Submitted 21 June, 2019; originally announced June 2019.

Comments: Extended version of MFCS 2019 paper

Quine's Fluted Fragment Revisited

Authors: I. Pratt-Hartmann, W. Szwast, L. Tendera

Abstract: We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified in 1968 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 $\mathcal{FL}^m$, the intersection of the fluted… ▽ More We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified in 1968 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 $\mathcal{FL}^m$, the intersection of the fluted fragment and the $m$-variable fragment of first-order logic, for all $m \geq 1$. We show that, for $m \geq 2$, this sub-fragment forces $\lfloor m/2\rfloor$-tuply exponentially large models, and that its satisfiability problem is $\lfloor m/2\rfloor$-NExpTime-hard. We further establish that, for $m \geq 3$, any satisfiable $\mathcal{FL}^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 $\mathcal{FL}^m$ for all $m \leq 4$. △ Less

Submitted 16 December, 2018; originally announced December 2018.

The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable

Authors: Ian Pratt-Hartmann

Abstract: We consider the two-variable fragment of first-order logic with one distinguished binary predicate constrained to be interpreted as a transitive relation. The finite satisfiability problem for this logic is shown to be decidable, in triply exponential non-deterministic time. The complexity falls to doubly exponential non-deterministic time if the distinguished binary predicate is constrained to be… ▽ More We consider the two-variable fragment of first-order logic with one distinguished binary predicate constrained to be interpreted as a transitive relation. The finite satisfiability problem for this logic is shown to be decidable, in triply exponential non-deterministic time. The complexity falls to doubly exponential non-deterministic time if the distinguished binary predicate is constrained to be interpreted as a partial order. △ Less

Submitted 18 July, 2017; originally announced July 2017.

Journal ref: Mathematical Logic Quarterly, 64(3), 2018, pp. 218--248

Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting

Authors: Georgios Kourtis, Ian Pratt-Hartmann

Abstract: 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. 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. △ Less

Submitted 27 October, 2017; v1 submitted 26 November, 2016; originally announced November 2016.

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 4 (October 30, 2017) lmcs:2557

Topological Logics with Connectedness over Euclidean Spaces

Authors: Roman Kontchakov, Yavor Nenov, Ian Pratt-Hartmann, Michael Zakharyaschev

Abstract: We consider the quantifier-free languages, Bc and Bc0, 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 n-dimensional Euclidean space (n greater than 1) and, additionally, over the regular closed… ▽ More We consider the quantifier-free languages, Bc and Bc0, 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 n-dimensional Euclidean space (n greater than 1) and, additionally, over the regular closed polyhedral sets of n-dimensional Euclidean space. 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 polyhedra in all dimensions greater than 1, and that the satisfiability problem for both languages is undecidable over both the regular closed sets and the regular closed polyhedra in the Euclidean plane. However, we also prove that the satisfiability problem for Bc0 is NP-complete over the regular closed sets in all dimensions greater than 2, while the corresponding problem for the regular closed polyhedra is ExpTime-complete. Our results show, in particular, that spatial reasoning over Euclidean spaces is much harder than reasoning over arbitrary topological spaces. △ Less

Submitted 18 October, 2011; originally announced October 2011.

MSC Class: 68T30 (Primary) 03D15; 68Q17 (Secondary) ACM Class: I.2.4; F.4.3; F.2.2

Journal ref: ACM Transactions on Computational Logic, 14(2:13), 2013

The Syllogistic with Unity

Authors: Ian Pratt-Hartmann

Abstract: We extend the language of the classical syllogisms with the sentence-forms "At most 1 p is a q" and "More than 1 p is a q". We show that the resulting logic does not admit a finite set of syllogism-like rules whose associated derivation relation is sound and complete, even when reductio ad absurdum is allowed. We extend the language of the classical syllogisms with the sentence-forms "At most 1 p is a q" and "More than 1 p is a q". We show that the resulting logic does not admit a finite set of syllogism-like rules whose associated derivation relation is sound and complete, even when reductio ad absurdum is allowed. △ Less

Submitted 11 October, 2011; originally announced October 2011.

MSC Class: 03B65 ACM Class: F.4.0

Journal ref: Journal of Philosophical Logic, 42(2),2013 , pp 391-407

On the Decidability of Connectedness Constraints in 2D and 3D Euclidean Spaces

Authors: Roman Kontchakov, Yavor Nenov, Ian Pratt-Hartmann, Michael Zakharyaschev

Abstract: 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-connectednes… ▽ More 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 the Euclidean plane, NP-complete over regular closed sets in three-dimensional Euclidean space, and ExpTime-complete over polyhedra in three-dimensional Euclidean space. △ Less

Submitted 1 April, 2011; originally announced April 2011.

Comments: Accepted for publication in the IJCAI 2011 proceedings

The Hamiltonian Syllogistic

Authors: Ian Pratt-Hartmann

Abstract: This paper undertakes a re-examination of Sir William Hamilton's doctrine of the quantification of the predicate. Hamilton's doctrine comprises two theses. First, the predicates of traditional syllogistic sentence-forms contain implicit existential quantifiers, so that, for example, "All p are q" is to be understood as "All p are some q". Second, these implicit quantifiers can be meaningfully dual… ▽ More This paper undertakes a re-examination of Sir William Hamilton's doctrine of the quantification of the predicate. Hamilton's doctrine comprises two theses. First, the predicates of traditional syllogistic sentence-forms contain implicit existential quantifiers, so that, for example, "All p are q" is to be understood as "All p are some q". Second, these implicit quantifiers can be meaningfully dualized to yield novel sentence-forms, such as, for example, "All p are all q". Hamilton attempted to provide a deductive system for his language, along the lines of the classical syllogisms. We show, using techniques unavailable to Hamilton, that such a system does exist, though with qualifications that distinguish it from its classical counterpart. △ Less

Submitted 12 November, 2010; originally announced November 2010.

Comments: 30 pages

MSC Class: 03B65 ACM Class: F.4.1; I.2.3

Journal ref: Journal of Logic, Language and Information, 20(4), 2011, pp. 445--474

Spatial logics with connectedness predicates

Authors: Roman Kontchakov, Ian Pratt-Hartmann, Frank Wolter, Michael Zakharyaschev

Abstract: We consider quantifier-free spatial logics, designed for qualitative spatial representation and reasoning in AI, and extend them with the means to represent topological connectedness of regions and restrict the number of their connected components. We investigate the computational complexity of these logics and show that the connectedness constraints can increase complexity from NP to PSpace, Exp… ▽ More We consider quantifier-free spatial logics, designed for qualitative spatial representation and reasoning in AI, and extend them with the means to represent topological connectedness of regions and restrict the number of their connected components. We investigate the computational complexity of these logics and show that the connectedness constraints can increase complexity from NP to PSpace, ExpTime and, if component counting is allowed, to NExpTime. △ Less

Submitted 18 October, 2010; v1 submitted 28 March, 2010; originally announced March 2010.

Comments: Some results of the paper were presented at LPAR 2008 and ECAI 2000

ACM Class: F.4.1, I.2.4

Journal ref: Logical Methods in Computer Science, Volume 6, Issue 3 (August 18, 2010) lmcs:1229

Complex Algebras of Arithmetic

Authors: Ivo Düntsch, Ian Pratt-Hartmann

Abstract: 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 n… ▽ More 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. △ Less

Submitted 1 December, 2009; v1 submitted 27 November, 2009; originally announced November 2009.

ACM Class: F.1.1

Journal ref: Fundamenta Informaticae, 97 (4), 2009, pp. 347-367

Functions Definable by Numerical Set-Expressions

Authors: Ian Pratt-Hartmann, Ivo Düntsch

Abstract: 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 lifti… ▽ More 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. △ Less

Submitted 31 October, 2009; originally announced November 2009.

ACM Class: F.1.1

Journal ref: Journal of Logic and Computation, 24(4), 2013, pp. 873-895

A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics

Authors: Yevgeny Kazakov, Ian Pratt-Hartmann

Abstract: Graded modal logic is the formal language obtained from ordinary (propositional) 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 investiga… ▽ More Graded modal logic is the formal language obtained from ordinary (propositional) 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. △ Less

Submitted 19 May, 2009; originally announced May 2009.

Comments: Full proofs for paper presented at the IEEE Conference on Logic in Computer Science, 2009

ACM Class: F.4.1; F.2.2

Journal ref: Proceedings, 24th Annual IEEE Symposium on Logic in Computer Science (LICS '09), IEEE Press, 2009, pp. 407--416

Logics for the Relational Syllogistic

Authors: Ian Pratt-Hartmann, Lawrence S. Moss

Abstract: The Aristotelian syllogistic cannot account for the validity of many inferences involving relational facts. In this paper, we investigate the prospects for providing a relational syllogistic. We identify several fragments based on (a) whether negation is permitted on all nouns, including those in the subject of a sentence; and (b) whether the subject noun phrase may contain a relative clause. Th… ▽ More The Aristotelian syllogistic cannot account for the validity of many inferences involving relational facts. In this paper, we investigate the prospects for providing a relational syllogistic. We identify several fragments based on (a) whether negation is permitted on all nouns, including those in the subject of a sentence; and (b) whether the subject noun phrase may contain a relative clause. The logics we present are extensions of the classical syllogistic, and we pay special attention to the question of whether reductio ad absurdum is needed. Thus our main goal is to derive results on the existence (or non-existence) of syllogistic proof systems for relational fragments. We also determine the computational complexity of all our fragments. △ Less

Submitted 4 August, 2008; originally announced August 2008.

ACM Class: F.4.1; I.2.3

Journal ref: Review of Symbolic Logic, 2(4), 2009, pp. 647--683

Data-Complexity of the Two-Variable Fragment with Counting Quantifiers

Authors: Ian Pratt-Hartmann

Abstract: The data-complexity of both satisfiability and finite satisfiability for the two-variable fragment with counting is NP-complete; the data-complexity of both query-answering and finite query-answering for the two-variable guarded fragment with counting is co-NP-complete. The data-complexity of both satisfiability and finite satisfiability for the two-variable fragment with counting is NP-complete; the data-complexity of both query-answering and finite query-answering for the two-variable guarded fragment with counting is co-NP-complete. △ Less

Submitted 10 June, 2008; originally announced June 2008.

ACM Class: F.4.1

Journal ref: Information and Computation, 207(8), 2009, pp. 867--888

On the Complexity of the Numerically Definite Syllogistic and Related Fragments

Authors: Ian Pratt-Hartmann

Abstract: In this paper, we determine the complexity of the satisfiability problem for various logics obtained by adding numerical quantifiers, and other constructions, to the traditional syllogistic. In addition, we demonstrate the incompleteness of some recently proposed proof-systems for these logics. In this paper, we determine the complexity of the satisfiability problem for various logics obtained by adding numerical quantifiers, and other constructions, to the traditional syllogistic. In addition, we demonstrate the incompleteness of some recently proposed proof-systems for these logics. △ Less

Submitted 6 January, 2007; originally announced January 2007.

Comments: 24 pages 1 figure

ACM Class: F.4.1

Journal ref: Bulletin of Symbolic Logic, 14(1), 2008, pp. 1--28

Complexity of the Guarded Two-Variable Fragment with Counting Quantifiers

Authors: Ian Pratt-Hartmann

Abstract: We show that the finite satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME. The method employed also yields a simple proof of a result recently obtained by Y. Kazakov, that the satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME. We show that the finite satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME. The method employed also yields a simple proof of a result recently obtained by Y. Kazakov, that the satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME. △ Less

Submitted 26 January, 2006; originally announced January 2006.

Comments: 20 pages, 3 figures

Journal ref: Journal of Logic and Computation, 17(1), 2007, pp. 133--155

Complexity of the Two-Variable Fragment with (Binary-Coded) Counting Quantifiers

Authors: Ian Pratt-Hartmann

Abstract: We show that the satisfiability and finite satisfiability problems for the two-variable fragment of first-order logic with counting quantifiers are both in NEXPTIME, even when counting quantifiers are coded succinctly. We show that the satisfiability and finite satisfiability problems for the two-variable fragment of first-order logic with counting quantifiers are both in NEXPTIME, even when counting quantifiers are coded succinctly. △ Less

Submitted 10 November, 2004; originally announced November 2004.

Comments: 24 pages, 1 pstex_t figure

ACM Class: F.4.1

Journal ref: Journal of Logic, Language and Information, 14(3), 2005, pp. 369--395