计算机科学中的逻辑

The correctness problem for reactive systems has been thoroughly explored and is well understood. Meanwhile, the efficiency problem for reactive systems has not received the same attention. Indeed, one correct system may be less fit than…

We investigate the equational theory of Kleene algebra terms with variable complements -- (language) complement where it applies only to variables -- w.r.t. languages. While the equational theory w.r.t. languages coincides with the language…

Weak memory models specify the semantics of concurrent programs on multi-core architectures. Reasoning techniques for weak memory models are often specialized to one fixed model and verification results are hence not transferable to other…

We identify multirole logic as a new form of logic in which conjunction/disjunction is interpreted as an ultrafilter on some underlying set of roles and the notion of negation is generalized to endomorphisms on this set. We formulate both…

We show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasoning tools. Theoretically, interactive protocols exist for all…

We give an algorithm for the class of second order unification problems in which second order variables have at most one occurrence.

Software changes frequently. To efficiently deal with such frequent changes, software verification tools must be incremental. Most of today's approaches for incremental verification consider one specific verification approach. One exception…

Normal form bisimilarities are a natural form of program equivalence resting on open terms, first introduced by Sangiorgi in call-by-name. The literature contains a normal form bisimilarity for Plotkin's call-by-value $\lambda$-calculus,…

Lookup tables (finite maps) are a ubiquitous data structure. In pure functional languages they are best represented using trees instead of hash tables. In pure functional languages within constructive logic, without a primitive integer…

We derive an intuitionistic version of G\"odel-L\"ob modal logic ($\sf{GL}$) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, $\sf{\ell IGL}$, by restricting a non-wellfounded labelled system for…

We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong L\"ob logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A…

We investigate the decidability of the ${0,\infty}$ fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL$^{0,\infty}$ is PSPACE-complete. Moreover, even its 1-variable fragment…

We present a variation of Hurkens paradox, which can itself be seen as a variation of Reynolds result that there is no set theoretic model of polymorphism.

Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be applicable to functional programs with higher-order types…

The notion of a Moore-Penrose inverse (M-P inverse) was introduced by Moore in 1920 and rediscovered by Penrose in 1955. The M-P inverse of a complex matrix is a special type of inverse which is unique, always exists, and can be computed…

Enabling preserving bisimilarity is a refinement of strong bisimilarity, which preserves safety as well as liveness properties. To define it properly, labelled transition systems needed to be upgraded with a successor relation, capturing…

Recently, several algorithms have been proposed for decomposing reactive synthesis specifications into independent and simpler sub-specifications. Being inspired by one of the approaches, developed by Antonio Iannopollo (2018), who designed…

Answer set programs in practice are often subject to change. This can lead to inconsistencies in the modified program due to conflicts between rules which are the results of the derivation of strongly complementary literals. To facilitate…

In answer set programming (ASP), answer sets capture solutions to search problems of interest and thus the efficient computation of answer sets is of utmost importance. One viable implementation strategy is provided by translation-based ASP…

Probabilistic logic programs are logic programs where some facts hold with a specified probability. Here, we investigate these programs with a causal framework that allows counterfactual queries. Learning the program structure from…