-
Decidability of Querying First-Order Theories via Countermodels of Finite Width
Authors:
Thomas Feller,
Tim S. Lyon,
Piotr Ostropolski-Nalewaja,
Sebastian Rudolph
Abstract:
We propose a generic framework for establishing the decidability of a wide range of logical entailment problems (briefly called querying), based on the existence of countermodels that are structurally simple, gauged by certain types of width measures (with treewidth and cliquewidth as popular examples). As an important special case of our framework, we identify logics exhibiting width-finite finit…
▽ More
We propose a generic framework for establishing the decidability of a wide range of logical entailment problems (briefly called querying), based on the existence of countermodels that are structurally simple, gauged by certain types of width measures (with treewidth and cliquewidth as popular examples). As an important special case of our framework, we identify logics exhibiting width-finite finitely universal model sets, warranting decidable entailment for a wide range of homomorphism-closed queries, subsuming a diverse set of practically relevant query languages. As a particularly powerful width measure, we propose Blumensath's partitionwidth, which subsumes various other commonly considered width measures and exhibits highly favorable computational and structural properties. Focusing on the formalism of existential rules as a popular showcase, we explain how finite partitionwidth sets of rules subsume other known abstract decidable classes but - leveraging existing notions of stratification - also cover a wide range of new rulesets. We expose natural limitations for fitting the class of finite unification sets into our picture and provide several options for remedy.
△ Less
Submitted 12 August, 2023; v1 submitted 13 April, 2023;
originally announced April 2023.
-
Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying
Authors:
Thomas Feller,
Tim S. Lyon,
Piotr Ostropolski-Nalewaja,
Sebastian Rudolph
Abstract:
In our pursuit of generic criteria for decidable ontology-based querying, we introduce 'finite-cliquewidth sets' (FCS) of existential rules, a model-theoretically defined class of rule sets, inspired by the cliquewidth measure from graph theory. By a generic argument, we show that FCS ensures decidability of entailment for a sizable class of queries (dubbed 'DaMSOQs') subsuming conjunctive queries…
▽ More
In our pursuit of generic criteria for decidable ontology-based querying, we introduce 'finite-cliquewidth sets' (FCS) of existential rules, a model-theoretically defined class of rule sets, inspired by the cliquewidth measure from graph theory. By a generic argument, we show that FCS ensures decidability of entailment for a sizable class of queries (dubbed 'DaMSOQs') subsuming conjunctive queries (CQs). The FCS class properly generalizes the class of finite-expansion sets (FES), and for signatures of arity at most 2, the class of bounded-treewidth sets (BTS). For higher arities, BTS is only indirectly subsumed by FCS by means of reification. Despite the generality of FCS, we provide a rule set with decidable CQ entailment (by virtue of first-order-rewritability) that falls outside FCS, thus demonstrating the incomparability of FCS and the class of finite-unification sets (FUS). In spite of this, we show that if we restrict ourselves to single-headed rule sets over signatures of arity at most 2, then FCS subsumes FUS.
△ Less
Submitted 6 September, 2022;
originally announced September 2022.
-
Symplectic cacti, virtualization and Berenstein-Kirillov groups
Authors:
Olga Azenhas,
Mojdeh Tarighat Feller,
Jacinta Torres
Abstract:
We explicitly realize an internal action of the symplectic cactus group, recently defined by Halacheva for any complex, reductive, finite-dimensional Lie algebra, on crystals of Kashiwara-Nakashima tableaux. Our methods include a symplectic version of jeu de taquin due to Sheats and Lecouvey, symplectic reversal, and virtualization due to Baker. As an application, we define and study a symplectic…
▽ More
We explicitly realize an internal action of the symplectic cactus group, recently defined by Halacheva for any complex, reductive, finite-dimensional Lie algebra, on crystals of Kashiwara-Nakashima tableaux. Our methods include a symplectic version of jeu de taquin due to Sheats and Lecouvey, symplectic reversal, and virtualization due to Baker. As an application, we define and study a symplectic version of the Berenstein-Kirillov group and show that it is a quotient of the symplectic cactus group. In addition two relations for symplectic Berenstein-Kirillov group are given that do not follow from the defining relations of the symplectic cactus group.
△ Less
Submitted 20 January, 2023; v1 submitted 18 July, 2022;
originally announced July 2022.
-
On Logics and Homomorphism Closure
Authors:
Manuel Bodirsky,
Thomas Feller,
Simon Knäuer,
Sebastian Rudolph
Abstract:
Predicate logic is the premier choice for specifying classes of relational structures. Homomorphisms are key to describing correspondences between relational structures. Questions concerning the interdependencies between these two means of characterizing (classes of) structures are of fundamental interest and can be highly non-trivial to answer. We investigate several problems regarding the homomo…
▽ More
Predicate logic is the premier choice for specifying classes of relational structures. Homomorphisms are key to describing correspondences between relational structures. Questions concerning the interdependencies between these two means of characterizing (classes of) structures are of fundamental interest and can be highly non-trivial to answer. We investigate several problems regarding the homomorphism closure (homclosure) of the class of all (finite or arbitrary) models of logical sentences: membership of structures in a sentence's homclosure; sentence homclosedness; homclosure characterizability in a logic; normal forms for homclosed sentences in certain logics. For a wide variety of fragments of first- and second-order predicate logic, we clarify these problems' computational properties.
△ Less
Submitted 29 June, 2021; v1 submitted 24 April, 2021;
originally announced April 2021.
-
Hardware-based Security for Virtual Trusted Platform Modules
Authors:
Sami Alsouri,
Thomas Feller,
Sunil Malipatlolla,
Stefan Katzenbeisser
Abstract:
Virtual Trusted Platform modules (TPMs) were proposed as a software-based alternative to the hardware-based TPMs to allow the use of their cryptographic functionalities in scenarios where multiple TPMs are required in a single platform, such as in virtualized environments. However, virtualizing TPMs, especially virutalizing the Platform Configuration Registers (PCRs), strikes against one of the co…
▽ More
Virtual Trusted Platform modules (TPMs) were proposed as a software-based alternative to the hardware-based TPMs to allow the use of their cryptographic functionalities in scenarios where multiple TPMs are required in a single platform, such as in virtualized environments. However, virtualizing TPMs, especially virutalizing the Platform Configuration Registers (PCRs), strikes against one of the core principles of Trusted Computing, namely the need for a hardware-based root of trust. In this paper we show how strength of hardware-based security can be gained in virtual PCRs by binding them to their corresponding hardware PCRs. We propose two approaches for such a binding. For this purpose, the first variant uses binary hash trees, whereas the other variant uses incremental hashing. In addition, we present an FPGA-based implementation of both variants and evaluate their performance.
△ Less
Submitted 7 August, 2013;
originally announced August 2013.
