计算机科学中的逻辑

We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based B\"uchi automata complementation. In particular, we propose a specialized rank-based construction for a Boolean combination of…

Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since, in particular via an extension of the temporal logic LTL…

This paper proves normalisation theorems for intuitionist and classical negative free logic, without and with the $\invertediota$ operator for definite descriptions. Rules specific to free logic give rise to new kinds of maximal formulas…

In this paper, we construct an interpretation-preserving functor from a category of concurrent games to the category of Scott domains and Scott-continuous functions. We give a concrete description of this functor, extending earlier results…

{\AA}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…

In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and…

Recent analysis of classical algorithms resulted in their axiomatization as transition systems satisfying some simple postulates, and in the formulation of the Abstract State Machine Theorem, which assures us that any classical algorithm…

In this paper, we study computational complexity and expressive power of modal operators for definite descriptions, which correspond to statements `the modal world which satisfies formula \(varphi\)'. We show that adding such operators to…

Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL.…

This work was presented in June 5-7, 2017 at the conference "Journ\'{e}es sur les Arithm\'{e}tiques Faibles -- Weak Arithmetics Days" held in Saint-Pertersburg of which no proceeding was ever published. It was not a new result but showed…

We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with "event bisimilarity"…

This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We…

Extended multi-adjoint logic programming arises as an extension of multi-adjoint normal logic programming where constraints and a special type of aggregator operator have been included. The use of this general aggregator operator permits to…

Formal Concept Analysis (FCA) is an approach to creating a conceptual hierarchy in which a \textit{concept lattice} is generated from a \textit{formal context}. That is, a triple consisting of a set of objects, $G$, a set of attributes,…

We provide the first generalized game characterization of van Glabbeek's linear-time--branching-time spectrum with silent steps. Thereby, one multi-dimensional energy game can be used to characterize and decide a wide array of weak…

Tape diagrams provide a convenient notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$, where $\otimes$ distributes over $\oplus $. In this work, we extend tape diagrams with…

This paper provides a set of cut-free complete sequent-style calculi for deontic STIT ('See To It That') logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting. We leverage these calculi to write…

A central task in knowledge compilation is to compile a CNF-SAT instance into a succinct representation format that allows efficient operations such as testing satisfiability, counting, or enumerating all solutions. Useful representation…

To obtain the highest confidence on the correction of numerical simulation programs for the resolution of Partial Differential Equations (PDEs), one has to formalize the mathematical notions and results that allow to establish the soundness…

We provide a category theoretical framework capturing two approaches to graph-based models of chemistry: formal reactions and disconnection rules. We model a translation from the latter to the former as a functor, which is faithful, and…