计算机科学中的逻辑

Binary multirelations can model alternating nondeterminism, for instance, in games or nondeterministically evolving systems interacting with an environment. Such systems can show partial or total functional behaviour at both levels of…

There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a unifying semantic…

The algebraic $\lambda$-calculus is an extension of the ordinary $\lambda$-calculus with linear combinations of terms. We establish that two ordinary $\lambda$-terms are equivalent in the algebraic $\lambda$-calculus iff they are…

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path…

Big data programming frameworks have become increasingly important for the development of applications for which performance and scalability are critical. In those complex frameworks, optimizing code by hand is hard and time-consuming,…

We introduce negation under the stable model semantics in DatalogMTL - a temporal extension of Datalog with metric temporal operators. As a result, we obtain a rule language which combines the power of answer set programming with the…

The set of pure terms which are typable in the $\lambda$$\Pi$-calculus in a given context is not recursive. So there is no general type inference algorithm for the programming language Elf and, in some cases, some type information has to be…

We discuss the deal of imperfectness of atomic actions in reality with the background of process algebras. And we show the applications of the imperfect actions in verification of computational systems.

This paper employs switching-algebraic techniques for the calculation of a fundamental index of voting powers, namely, the total Banzhaf power. This calculation involves two distinct operations: (a) Boolean differencing or differentiation,…

Capturing stochastic behaviors in business and work processes is essential to quantitatively understand how nondeterminism is resolved when taking decisions within the process. This is of special interest in process mining, where event data…

Binary multirelations form a model of alternating nondeterminism useful for analysing games, interactions of computing systems with their environments or abstract interpretations of probabilistic programs. We investigate this alternating…

In this paper, we address program development by multiple different programmers (or programming teams), each working in different settings (programming languages or reasoning frameworks), but following a common specification; in particular,…

We prove that the pattern matching problem is undecidable in polymorphic lambda-calculi (as Girard's system F) and calculi supporting inductive types (as G{\"o}del's system T) by reducing Hilbert's tenth problem to it. More generally…

We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with $\eta$-conversion. Because these systems verify the proofs-as-objects paradigm, the proof synthesis method is a one level process…

Runtime assurance (RTA) addresses the problem of keeping an autonomous system safe while using an untrusted (or experimental) controller. This can be done via logic that explicitly switches between the untrusted controller and a safety…

A key goal of the System-Theoretic Process Analysis (STPA) hazard analysis technique is the identification of loss scenarios - causal factors that could potentially lead to an accident. We propose an approach that aims to assist engineers…

Deciding formulas mixing arithmetic and uninterpreted predicates is of practical interest, notably for applications in verification. Some decision procedures consist in building by structural induction an automaton that recognizes the set…

First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in finite-domain first-order logic. In this paper, we argue that the capabilities of FOMC algorithms to date are limited by their…

We extend to general Cartesian categories the idea of Coherent Differentiation recently introduced by Ehrhard in the setting of categorical models of Linear Logic. The first ingredient is a summability structure which induces a partial…

We introduce categories of extended Gaussian maps and Gaussian relations which unify Gaussian probability distributions with relational nondeterminism in the form of linear relations. Both have crucial and well-understood applications in…