相关论文: Finite Model Property and Bisimulation for LFD

We study hidden-variable models from quantum mechanics, and their abstractions in purely probabilistic and relational frameworks, by means of logics of dependence and independence, based on team semantics. We show that common desirable…

We introduce the notion of bilinear moment functional and study their general properties. The analogue of Favard's theorem for moment functionals is proven. The notion of semi-classical bilinear functionals is introduced as a generalization…

We extend first-order logic to include variadic function symbols, and prove a substitution lemma. Two applications are given: one to bounded quantifier elimination and one to the definability of certain Borel sets.

Classical logics of knowledge and belief are usually interpreted on Kripke models, for which a mathematically well-developed model theory is available. However, such models are inadequate to capture dynamic phenomena. Therefore, epistemic…

Labeled state-to-function transition systems, FuTS for short, are characterized by transitions which relate states to functions of states over general semirings, equipped with a rich set of higher-order operators. As such, FuTS constitute a…

A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. The proofs of soundness and completeness are constructive and…

The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was…

The satisfiability problem for First-order Modal Logic (\FOML) is undecidable even for simple fragments like having only unary predicates, two variables etc. Recently a new way to identify decidable fragments of \FOML has been introduced…

Formal verification using the model checking paradigm has to deal with two aspects: The system models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of…

Inquisitive modal logic, InqML, in its epistemic incarnation, extends standard epistemic logic to capture not just the information that agents have, but also the questions that they are interested in. We use the natural notion of…

We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems,…

We study a many-valued generalization of Propositional Dynamic Logic where formulas in states and accessibility relations between states of a Kripke model are evaluated in a finite FL-algebra. One natural interpretation of this framework is…

Bounded Derivation Depth property (BDD) and Finite Controllability (FC) are two properties of sets of datalog rules and tuple generating dependencies (known as Datalog +/- programs), which recently attracted some attention. We conjecture…

Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (FO+lfp) with background theories. Such logics, unlike pure…

Many forms of dependence manifest themselves over time, with behavior of variables in dynamical systems as a paradigmatic example. This paper studies temporal dependence in dynamical systems from a logical perspective, by enriching a…

We study probabilistic complexity classes and questions of derandomisation from a logical point of view. For each logic L we introduce a new logic BPL, bounded error probabilistic L, which is defined from L in a similar way as the…

We define and study logics in the framework of probabilistic team semantics and over metafinite structures. Our work is paralleled by the recent development of novel axiomatizable and tractable logics in team semantics that are closed under…

Let $X$ be an $F$-finite smooth scheme of essentially finite type over a perfect field. This article proves the existence of $b$-functions for locally finitely generated unit $F$-modules when equipped with their induced…

Fuzzy Description Logics (DLs) are a family of logics which allow the representation of (and the reasoning with) structured knowledge affected by vagueness. Although most of the not very expressive crisp DLs, such as ALC, enjoy the Finite…

Inquisitive modal logic InqML is a generalisation of standard Kripke-style modal logic. In its epistemic incarnation, it extends standard epistemic logic to capture not just the information that agents have, but also the questions that they…