计算机科学中的逻辑

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,…

In this paper, we present a logic for conditional strong historical necessity in branching time and apply it to analyze a nontheological version of Lavenham's argument for future determinism. Strong historical necessity is motivated from a…

We introduce a simple natural deduction system for reasoning with judgments of the form "there exists a proof of $\varphi$" to explore the notion of judgmental existence following Martin-L\"{o}f's methodology of distinguishing between…

We initiate the study of counting Markov Equivalence Classes (MEC) under logical constraints. MECs are equivalence classes of Directed Acyclic Graphs (DAGs) that encode the same conditional independence structure among the random variables…

The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as…

Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state. Hyperproperties are properties…

Analogical reasoning is the ability to detect parallels between two seemingly distant objects or situations, a fundamental human capacity used for example in commonsense reasoning, learning, and creativity which is believed by many…

We record a particularly simple construction on top of Lumsdaine's local universes that allows for a Coquand-style universe of propositions with propositional extensionality to be interpreted in a category with subobject classifiers.

A linear constraint loop is specified by a system of linear inequalities that define the relation between the values of the program variables before and after a single execution of the loop body. In this paper we consider the problem of…

Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical formulation of this problem, where operations on state-based…

We study the expressivity and the complexity of various logics in probabilistic team semantics with the Boolean negation. In particular, we study the extension of probabilistic independence logic with the Boolean negation, and a recently…

The purpose of these notes is to give a categorical semantics for the transpension type (Nuyts and Devriese, Transpension: The Right Adjoint to the Pi-type, Accepted at LMCS, 2024), which is right adjoint to a potentially substructural…

The problem of counting the number of models of a given Boolean formula has numerous applications, including computing the leakage of deterministic programs in Quantitative Information Flow. Model counting is a hard, #P-complete problem.…

Using an iterative tree construction we show that for simple computable subsets of the Cantor space Hausdorff, constructive and computable dimensions might be incomputable.

In probabilistic updating one transforms a prior distribution in the light of given evidence into a posterior distribution, via what is called conditioning, updating, belief revision or inference. This is the essence of learning, as…

RA is a software package that couples machine learning with formal reasoning in an attempt to find the laws that generate the empirical data that it has been given access to. A brief outline of RA in its initial stage of development is…

This paper proposes a novel method for automatically inferring message flow specifications from the communication traces of a system-on-chip (SoC) design that captures messages exchanged among the components during a system execution. The…

The initial algebra for an endofunctor F provides a recursion and induction scheme for data structures whose constructors are described by F. The initial-algebra construction by Ad\'amek (1974) starts with the initial object (e.g. the empty…

The formal XAI community has studied a plethora of interpretability queries aiming to understand the classifications made by decision trees. However, a more uniform understanding of what questions we can hope to answer about these models,…

We revisit evaluation of logical formulas that allow both uninterpreted relations, constrained to be finite, as well as an interpreted vocabulary over an infinite domain. This formalism was denoted embedded finite model theory in the past.…