计算机科学中的逻辑

Markov Decision Processes (MDPs) model systems with uncertain transition dynamics. Multiple-environment MDPs (MEMDPs) extend MDPs. They intuitively reflect finite sets of MDPs that share the same state and action spaces but differ in the…

This paper addresses objectives tailored to the risk-averse optimization of accumulated rewards in Markov decision processes (MDPs). The studied objectives require maximizing the expected value of the accumulated rewards minus a penalty…

We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results…

Slot machines can have fairly complex behaviour. Determining the RTP (return to player) can be involved, especially when a player has an influence on the course of the game. In this paper we model the behaviour of slot machines using…

Parametricity allows the transfer of proofs between different implementations of the same data structure. The lambdaPi-calculus modulo theory is an extension of the lambda-calculus with dependent types and user-defined rewrite rules. It is…

Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translation to higher-order logic. In this paper, we adapt it for…

When reasoning about formal objects whose structures involve binding, it is often necessary to analyze expressions relative to a context that associates types, values, and other related attributes with variables that appear free in the…

The "Harmony Lemma", as formulated by Sangiorgi & Walker, establishes the equivalence between the labelled transition semantics and the reduction semantics in the $\pi$-calculus. Despite being a widely known and accepted result for the…

We present GS (Guarded Successor), a novel decidable temporal logic with several unique distinctive features. Among those, it allows infinitely many data values that come not only with equality but with a somehow rich theory too: the…

When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and…

This paper leans on two similar areas so far detached from each other. On the one hand, Dung's pioneering contributions to abstract argumentation, almost thirty years ago, gave rise to a plethora of successors, including abstract…

Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in…

The support for higher-order reasoning in the Vampire theorem prover has recently been completely reworked. This rework consists of new theoretical ideas, a new implementation, and a dedicated strategy schedule. The theoretical ideas are…

We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in which we can not only compose and execute code, but also…

We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechanization is achieved via a shallow semantical embedding in…

In a previous publication, we introduced an abstract logic via an abstract notion of quantifier. Drawing upon concepts from categorical logic, this abstract logic interprets formulas from context as subobjects in a specific category, e.g.,…

We study networks of processes that all execute the same finite state protocol and that communicate through broadcasts. The processes are organized in a graph (a topology) and only the neighbors of a process in this graph can receive its…

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity…

For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among these methods, differentiable logics (DLs) are used to…

We introduce a single-set axiomatisation of cubical $\omega$-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical $\omega$-categories,…