Knowability As Continuity: The Modal Logic of Continuous and Uniform Dependence
ABSTRACT. I investigate modal logics for various forms of functional dependence between variables in topological spaces. The motivation is epistemic, the aim being to model and study knowable informational dependence between empirical questions (for which only approximate answers are empirically observable). In this context, knowability of the dependence corresponds to continuity of the underlying function. I also investigate epistemic independence in topological terms and show that it is compatible with functional (but non-continuous) dependence. I then proceed to study a stronger notion of knowability based on uniformly continuous dependence. On the technical logical side, I determine the complete logics of languages that combine general functional dependence, continuous dependence, and uniformly continuous dependence. This talk is based on recent joint work with Johan van Benthem.
ABSTRACT. The field of product modal logics was extensively developed in the last two decades. One of the simplest logic in this family is the product S5×S5 (S5^2). In this paper, we explore the complexity of a specific instance of S5^2, called PLC (Product modal Logic of Classifiers), which was recently proposed in the field of logic-based explainable AI to model "black box" classifiers and their explanations. The PLC semantics gives concrete meanings to the two dimensions: the first ranges over the possible input instances to be classified and the other over the possible classifiers. We will show that, unlike S5^2 whose satisfiability problem is known to be NEXPTIME-complete, the satisfiability problem of PLC is simply EXPTIME-complete. This is due to the computationally grounded nature of PLC in comparison with S5^2 and, in particular, to the fact that along one of its two dimensions only classifications can vary while values of atomic propositions representing input instances stay the same.
LEGO-like Small Model Constructions for Åqvist’s Logics
ABSTRACT. Åqvist's logics (E, F, F+(CM), and G) are among the best-known systems in the long tradition of preference-based approaches for modeling conditional obligation. While the general semantics of preference models align well with philosophical intuitions, more constructive characterizations are needed to assess computational complexity and facilitate automated deduction. Existing small model constructions from conditional logics (due to Friedman and Halpern) are applicable only to F+(CM) and G, while recently developed proof-theoretic characterizations leave unresolved the exact complexity of theoremhood in logic F. In this paper, we introduce alternative small model constructions assembled from elementary building blocks, applicable uniformly to all four Åqvist's logics. Our constructions propose alternative semantical characterizations and imply co-NP-completeness of theoremhood. Furthermore, they can be naturally encoded in classical propositional logic for automated deduction.
ABSTRACT. All the binomial lattices embed into $\QI$, the complete lattice ofsup-preserving endomaps of the unit interval---whose elements can beseen as continuous monotone paths from $(0,0)$ to $(1,1)$. Thislattice is \cd. We give a general description of the completecongruences of \cdlatt{s} by means of an interior operator on thecollection of closed subsets of an associated topological space. Inparticular, we show that these form a frame. We give a description ofthis frame for the unit interval lattice, showing that it is not aBoolean algebra nor a (co)spatial frame. For $\QI$, we give ageometrical interpretation of these congruences by means of directedhomotopies.
ABSTRACT. Software generators that compile and deploy a specification into a functional information system can help to increase the frequency of releases in the software process. They achieve this by reducing development time and minimizing human-induced errors. However, many software generators lack support for data migration. This can inhibit a steady pace of releases, especially for increments that alter the system's schema in production. Consequently, schema-changing data migrations often face challenges, leading developers to resort to manual migration or employ workarounds.
To address this issue, this paper proposes a \foundtheory{} for data migration, aiming to generate migration scripts for automating the migration process. The overarching challenge is preserving the business semantics of data amidst schema changes. Specifically, this paper tackles the task of generating a migration script based on the schemas of both the existing and the desired system, under the condition of zero downtime. The proposed solution was validated by a prototype demonstrating its efficacy. Notably, the \ourtheory{} is technology-independent, articulating systems in terms of invariants, thereby ensuring applicability across various scenarios. The migration script generator will be implemented in a software generator named Ampersand.
The exact correspondence between intuitionistic and modal logic
ABSTRACT. A normalizing system of classical natural deduction for S4 is given. It is shown that steps of indirect proof can be eliminated from derivations of formulas T(A) translated from intuitionistic logic to S4. For the converse translation, the modal operators and their rules are simply deleted, to obtain a derivation of A in intuitionistic logic.
ABSTRACT. We introduce a series of models of various modal logics built out of structures of ultrafilters on the algebra of premodal propositions. Given a pointed modal model, we give a general method for constructing a bisimilar pointed model using trees of indexed ultrafilters. At the end, we examine philosophical applications to accounts of metaphysical necessity.
ABSTRACT. We study products of unimodal logics characterized by classes of Kripke frames defined by universal Horn formulas, classifying them with respect to the finite model property (FMP). Further, we show that products of modal logics defined only with variable-free axioms have the FMP. We also provide a partial result regarding products of logics with both Horn and variable-free axioms.
First-order Probabilistic Logic with Sequence Variables and Unranked Symbols
ABSTRACT. We present an unranked probabilistic logic, which is an extension of the first-order probability logic with sequence variables and flexible-arity (unranked) function and predicate symbols. The semantics of the logic is defined using Kripke worlds and the strong completeness theorem holds for it. Such a formalism is interesting as it provides very flexible and expressive platform to model various problems coming from real world applications.
ABSTRACT. This note investigates the algebraic semantics of fuzzy modal logics from the point of view of quantale-enriched category theory. The set of truth-values (distances) is given by a complete lattice $\Omega$ with a (non-commutative) multiplication. Notions such as set, function, relation, downset, upset, (co)limit will be ``internalized'' in $\Omega$. Algebras are equipped with a metric, functions are distance non-increasing, relations are fuzzy and (co)limits include not only meets and joins but unary modalities known as power and tensor. Our main contribution is to show that the canonical extensions known in order theory generalize to the setting of quantale-enriched category theory.
Nested proof theory for quasi-transitive modal logics
ABSTRACT. Previous works by Goré and co-authors have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent.
Our aim is to provide (i) a constructive cut-elimination procedure and (ii) alternative modular formulations for these systems.
We present our methodology to achieve these two goals on a subclass of path axioms, namely quasi-transitivity axioms, and discuss how it could be extended further to quasi-symmetry axioms.
ABSTRACT. The question of characterizing the (finite) representable relation algebras in a “nice" way is open. The class RRA is known to be not finitely axiomatizable in first-order logic. Nevertheless, it is conjectured that “almost all” finite relation algebras are representable.
All finite relation algebras with three or fewer atoms are representable. So one may ask, Over what cardinalities of sets are they representable? This question was answered completely by Andréka and Maddux (“Rep- resentations for small relation algebras,” Notre Dame J. Form. Log., 35 (1994)); they determine the spectrum of every finite relation algebra with three or fewer atoms.
In the present paper, we restrict attention to cyclic group representations, and completely determine the cyclic group spectrum for all seven sym- metric integral relation algebras on three atoms. We find that in some instances, the spectrum and cyclic spectrum agree; in other instances, the spectra disagree for finitely many n; finally, for other instances, the spectra disagree for infinitely many n. The proofs employ constructions, SAT solvers, and the probabilistic method.
ABSTRACT. Interval-order partially ordered multisets with interfaces (ipomsets) have shown to be a versatile model for executions of concurrent systems in which both precedence and concurrency need to be taken into account.
In this paper, we develop a presentation of ipomsets as generated by a graph of certain discrete ipomsets (starters and terminators) under the relation which composes subsequent starters and subsequent terminators. Using this presentation, we show that also subsumptions are generated by elementary relations. We develop a similar correspondence on the automata side, relating higher-dimensional automata, which generate ipomsets, and ST-automata, which generate step sequences, and their respective languages.