arXiv subjects

Balder ten Cate

Publications and source records attributed to Balder ten Cate.

At least 37 records · Page 2Linked to original sources

arXiv2024

Characterising Modal Formulas with Examples

We study the existence of finite characterisations for modal formulas. A finite characterisation of a modal formula $φ$ is a finite collection of positive and negative examples that distinguishes $φ$ from every other, non-equivalent modal formula, where an example is a finite pointed Kripke structure. This definition can be restricted to specific frame classes and to fragments of the modal language: a modal fragment $L$ admits finite characterisations with respect to a frame class $F$ if every formula $φ\in L$ has a finite characterisation with respect to $L$ consting of examples that are based on frames in $F$. Finite characterisations are useful for illustration, interactive specification, and debugging of formal specifications, and their existence is a precondition for exact learnability with membership queries. We show that the full modal language admits finite characterisations with respect to a frame class $F$ only when the modal logic of $F$ is locally tabular. We then study which modal fragments, freely generated by some set of connectives, admit finite characterisations. Our main result is that the positive modal language without the truth-constants $\top$ and $\bot$ admits finite characterisations w.r.t. the class of all frames. This result is essentially optimal: finite characterizability fails when the language is extended with the truth constant $\top$ or $\bot$ or with all but very limited forms of negation.

cs.LO↗

arXiv2024

When do homomorphism counts help in query algorithms?

A query algorithm based on homomorphism counts is a procedure for determining whether a given instance satisfies a property by counting homomorphisms between the given instance and finitely many predetermined instances. In a left query algorithm, we count homomorphisms from the predetermined instances to the given instance, while in a right query algorithm we count homomorphisms from the given instance to the predetermined instances. Homomorphisms are usually counted over the semiring N of non-negative integers; it is also meaningful, however, to count homomorphisms over the Boolean semiring B, in which case the homomorphism count indicates whether or not a homomorphism exists. We first characterize the properties that admit a left query algorithm over B by showing that these are precisely the properties that are both first-order definable and closed under homomorphic equivalence. After this, we turn attention to a comparison between left query algorithms over B and left query algorithms over N. In general, there are properties that admit a left query algorithm over N but not over B. The main result of this paper asserts that if a property is closed under homomorphic equivalence, then that property admits a left query algorithm over B if and only if it admits a left query algorithm over N. In other words and rather surprisingly, homomorphism counts over N do not help as regards properties that are closed under homomorphic equivalence. Finally, we characterize the properties that admit both a left query algorithm over B and a right query algorithm over B.

cs.LO↗

arXiv2023

Extremal Fitting CQs do not Generalize

A fitting algorithm for conjunctive queries (CQs) produces, given a set of positively and negatively labeled data examples, a CQ that fits these examples. In general, there may be many non-equivalent fitting CQs and thus the algorithm has some freedom in producing its output. Additional desirable properties of the produced CQ are that it generalizes well to unseen examples in the sense of PAC learning and that it is most general or most specific in the set of all fitting CQs. In this research note, we show that these desiderata are incompatible when we require PAC-style generalization from a polynomial sample: we prove that any fitting algorithm that produces a most-specific fitting CQ cannot be a sample-efficient PAC learning algorithm, and the same is true for fitting algorithms that produce a most-general fitting CQ (when it exists). Our proofs rely on a polynomial construction of relativized homomorphism dualities for path-shaped structures.

cs.DB↗

arXiv2023

On the non-efficient PAC learnability of conjunctive queries

This note serves three purposes: (i) we provide a self-contained exposition of the fact that conjunctive queries are not efficiently learnable in the Probably-Approximately-Correct (PAC) model, paying clear attention to the complicating fact that this concept class lacks the polynomial-size fitting property, a property that is tacitly assumed in much of the computational learning theory literature; (ii) we establish a strong negative PAC learnability result that applies to many restricted classes of conjunctive queries (CQs), including acyclic CQs for a wide range of notions of "acyclicity"; (iii) we show that CQs (and UCQs) are efficiently PAC learnable with membership queries.

cs.DB↗

arXiv2023

SAT-Based PAC Learning of Description Logic Concepts

We propose bounded fitting as a scheme for learning description logic concepts in the presence of ontologies. A main advantage is that the resulting learning algorithms come with theoretical guarantees regarding their generalization to unseen examples in the sense of PAC learning. We prove that, in contrast, several other natural learning algorithms fail to provide such guarantees. As a further contribution, we present the system SPELL which efficiently implements bounded fitting for the description logic $\mathcal{ELH}^r$ based on a SAT solver, and compare its performance to a state-of-the-art learner.

cs.AI↗

arXiv2023

Craig Interpolation for Guarded Fragments

We show that the guarded-negation fragment (GNFO) is, in a precise sense, the smallest extension of the guarded fragment (GFO) with Craig interpolation. In contrast, %we show that the smallest extension of the two-variable fragment (FO2) with Craig interpolation is full first-order logic.

cs.LO↗

arXiv2023

Right-Adjoints for Datalog Programs, and Homomorphism Dualities over Restricted Classes

A Datalog program can be viewed as a syntactic specification of a functor from database instances over some schema to database instances over another schema. The same holds more generally for $\exists$Datalog. We establish large classes of Datalog and $\exists$Datalog programs for which the corresponding functor admits a generalized right-adjoint. We employ these results to obtain new insights into the existence of, and methods for constructing, homomorphism dualities within restricted classes of instances. We also derive new results regarding the existence of uniquely characterizing data examples for database queries.

cs.LO↗

arXiv2022

Conjunctive Queries: Unique Characterizations and Exact Learnability

We answer the question which conjunctive queries are uniquely characterized by polynomially many positive and negative examples, and how to construct such examples efficiently. As a consequence, we obtain a new efficient exact learning algorithm for a class of conjunctive queries. At the core of our contributions lie two new polynomial-time algorithms for constructing frontiers in the homomorphism lattice of finite structures. We also discuss implications for the unique characterizability and learnability of schema mappings and of description logic concepts.

cs.LO↗

arXiv2022

Local Dependence and Guarding

We study LFD, a base logic of functional dependence introduced by Baltag and van Benthem (2021) and its connections with the guarded fragment GF of first-order logic. Like other logics of dependence, the semantics of LFD uses teams: sets of permissible variable assignments. What sets LFD apart is its ability to express local dependence between variables and local dependence of statements on variables. Known features of LFD include decidability, explicit axiomatization, finite model property, and a bisimulation characterization. Others, including the complexity of satisfiability, remained open so far. More generally, what has been lacking is a good understanding of what makes the LFD approach to dependence computationally well-behaved, and how it relates to other decidable logics. In particular, how do allowing variable dependencies and guarding quantifiers compare as logical devices? We provide a new compositional translation from GF into LFD, and conversely, we translate LFD into GF in an `almost compositional' manner. Using these two translations, we transfer known results about GF to LFD in a uniform manner, yielding, e.g., tight complexity bounds for LFD satisfiability, as well as Craig interpolation. Conversely, e.g., the finite model property of LFD transfers to GF. Thus, local dependence and guarding turn out to be intricately entangled notions.

cs.LO↗

arXiv2022

Characterising Modal Formulas with Examples

We initiate the study of finite characterizations and exact learnability of modal languages. A finite characterization of a modal formula w.r.t. a set of formulas is a finite set of finite models (labelled either positive or negative) which distinguishes this formula from every other formula from that set. A modal language L admits finite characterisations if every L-formula has a finite characterization w.r.t. L. This definition can be applied not only to the basic modal logic K, but to arbitrary normal modal logics. We show that a normal modal logic admits finite characterisations (for the full modal language) iff it is locally tabular. This shows that finite characterizations with respect to the full modal language are rare, and hence motivates the study of finite characterizations for fragments of the full modal language. Our main result is that the positive modal language without the truth-constants $\top$ and $\bot$ admits finite characterisations. Moreover, we show that this result is essentially optimal: finite characterizations no longer exist when the language is extended with the truth constant $\bot$ or with all but very limited forms of negation.

cs.LO↗

arXiv2020

Some Model Theory of Guarded Negation

The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this paper we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics. This version of the paper contains streamlined and corrected versions of results concerning entailment of a conjunctive query from a set of ground facts and a theory consisting of GNFO sentences of a special form ("dependencies").

cs.LO↗

arXiv2019

Learning Multilingual Word Embeddings Using Image-Text Data

There has been significant interest recently in learning multilingual word embeddings -- in which semantically similar words across languages have similar embeddings. State-of-the-art approaches have relied on expensive labeled data, which is unavailable for low-resource languages, or have involved post-hoc unification of monolingual embeddings. In the present paper, we investigate the efficacy of multilingual embeddings learned from weakly-supervised image-text data. In particular, we propose methods for learning multilingual embeddings using image-text data, by enforcing similarity between the representations of the image and that of the text. Our experiments reveal that even without using any expensive labeled data, a bag-of-words-based embedding model trained on image-text data achieves performance comparable to the state-of-the-art on crosslingual semantic similarity tasks.

cs.CL↗

arXiv2018

Recursive Programs for Document Spanners

A document spanner models a program for Information Extraction (IE) as a function that takes as input a text document (string over a finite alphabet) and produces a relation of spans (intervals in the document) over a predefined schema. A well studied language for expressing spanners is that of the regular spanners: relational algebra over regex formulas, which are obtained by adding capture variables to regular expressions. Equivalently, the regular spanners are the ones expressible in non-recursive Datalog over regex formulas (extracting relations that play the role of EDBs from the input document). In this paper, we investigate the expressive power of recursive Datalog over regex formulas. Our main result is that such programs capture precisely the document spanners computable in polynomial time. Additional results compare recursive programs to known formalisms such as the language of core spanners (that extends regular spanners by allowing to test for string equality) and its closure under difference. Finally, we extend our main result to a recently proposed framework that generalizes both the relational model and document spanners.

cs.DB↗

arXiv2018

Inference From Visible Information And Background Knowledge

We provide a wide-ranging study of the scenario where a subset of the relations in a relational vocabulary are visible to a user --- that is, their complete contents are known --- while the remaining relations are invisible. We also have a background theory --- invariants given by logical sentences --- which may relate the visible relations to invisible ones, and also may constrain both the visible and invisible relations in isolation. We want to determine whether some other information, given as a positive existential formula, can be inferred using only the visible information and the background theory. This formula whose inference we are concered with is denoted as the \emph{query}. We consider whether positive information about the query can be inferred, and also whether negative information -- the sentence does not hold -- can be inferred. We further consider both the instance-level version of the problem, where both the query and the visible instance are given, and the schema-level version, where we want to know whether truth or falsity of the query can be inferred in some instance of the schema.

cs.LO↗

arXiv2015

Exchange-Repairs: Managing Inconsistency in Data Exchange

In a data exchange setting with target constraints, it is often the case that a given source instance has no solutions. In such cases, the semantics of target queries trivialize. The aim of this paper is to introduce and explore a new framework that gives meaningful semantics in such cases by using the notion of exchange-repairs. Informally, an exchange-repair of a source instance is another source instance that differs minimally from the first, but has a solution. Exchange-repairs give rise to a natural notion of exchange-repair certain answers (XR-certain answers) for target queries. We show that for schema mappings specified by source-to-target GAV dependencies and target equality-generating dependencies (egds), the XR-certain answers of a target conjunctive query can be rewritten as the consistent answers (in the sense of standard database repairs) of a union of conjunctive queries over the source schema with respect to a set of egds over the source schema, making it possible to use a consistent query-answering system to compute XR-certain answers in data exchange. We then examine the general case of schema mappings specified by source-to-target GLAV constraints, a weakly acyclic set of target tgds and a set of target egds. The main result asserts that, for such settings, the XR-certain answers of conjunctive queries can be rewritten as the certain answers of a union of conjunctive queries with respect to the stable models of a disjunctive logic program over a suitable expansion of the source schema.

cs.DB↗

arXiv2015

High-Level Why-Not Explanations using Ontologies

We propose a novel foundational framework for why-not explanations, that is, explanations for why a tuple is missing from a query result. Our why-not explanations leverage concepts from an ontology to provide high-level and meaningful reasons for why a tuple is missing from the result of a query. A key algorithmic problem in our framework is that of computing a most-general explanation for a why-not question, relative to an ontology, which can either be provided by the user, or it may be automatically derived from the data and/or schema. We study the complexity of this problem and associated problems, and present concrete algorithms for computing why-not explanations. In the case where an external ontology is provided, we first show that the problem of deciding the existence of an explanation to a why-not question is NP-complete in general. However, the problem is solvable in polynomial time for queries of bounded arity, provided that the ontology is specified in a suitable language, such as a member of the DL-Lite family of description logics, which allows for efficient concept subsumption checking. Furthermore, we show that a most-general explanation can be computed in polynomial time in this case. In addition, we propose a method for deriving a suitable (virtual) ontology from a database and/or a data workspace schema, and we present an algorithm for computing a most-general explanation to a why-not question, relative to such ontologies. This algorithm runs in polynomial-time in the case when concepts are defined in a selection-free language, or if the underlying schema is fixed. Finally, we also study the problem of computing short most-general explanations, and we briefly discuss alternative definitions of what it means to be an explanation, and to be most general.

cs.DB↗

arXiv2015

Declarative Statistical Modeling with Datalog

Formalisms for specifying statistical models, such as probabilistic-programming languages, typically consist of two components: a specification of a stochastic process (the prior), and a specification of observations that restrict the probability space to a conditional subspace (the posterior). Use cases of such formalisms include the development of algorithms in machine learning and artificial intelligence. We propose and investigate a declarative framework for specifying statistical models on top of a database, through an appropriate extension of Datalog. By virtue of extending Datalog, our framework offers a natural integration with the database, and has a robust declarative semantics. Our Datalog extension provides convenient mechanisms to include numerical probability functions; in particular, conclusions of rules may contain values drawn from such functions. The semantics of a program is a probability distribution over the possible outcomes of the input database with respect to the program; these outcomes are minimal solutions with respect to a related program with existentially quantified variables in conclusions. Observations are naturally incorporated by means of integrity constraints over the extensional and intensional relations. We focus on programs that use discrete numerical distributions, but even then the space of possible outcomes may be uncountable (as a solution can be infinite). We define a probability measure over possible outcomes by applying the known concept of cylinder sets to a probabilistic chase procedure. We show that the resulting semantics is robust under different chases. We also identify conditions guaranteeing that all possible outcomes are finite (and then the probability space is discrete). We argue that the framework we propose retains the purely declarative nature of Datalog, and allows for natural specifications of statistical models.

cs.DB↗

arXiv2013

Unary negation

We study fragments of first-order logic and of least fixed point logic that allow only unary negation: negation of formulas with at most one free variable. These logics generalize many interesting known formalisms, including modal logic and the $μ$-calculus, as well as conjunctive queries and monadic Datalog. We show that satisfiability and finite satisfiability are decidable for both fragments, and we pinpoint the complexity of satisfiability, finite satisfiability, and model checking. We also show that the unary negation fragment of first-order logic is model-theoretically very well behaved. In particular, it enjoys Craig Interpolation and the Projective Beth Property.

cs.LO↗