计算机科学中的逻辑

In this paper, we explore a quantitative approach to querying inconsistent description logic knowledge bases. We consider weighted knowledge bases in which both axioms and assertions have (possibly infinite) weights, which are used to…

Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A particular feature is pipelined "out-of-order execution" of the…

Dependency pairs constitute a series of very effective techniques for the termination analysis of term rewriting systems. In this paper, we adapt the static dependency pair framework to logically constrained simply-typed term rewriting…

Which dynamic queries can be maintained efficiently? For constant-size changes, it is known that constant-depth circuits or, equivalently, first-order updates suffice for maintaining many important queries, among them reachability, tree…

This paper describes a formal theory of smooth vector fields, Lie groups and the Lie algebra of a Lie group in the theorem prover Isabelle. Lie groups are abstract structures that are composable, invertible and differentiable. They are…

We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specification language for OCaml that can be used both in dynamic and…

Quantum finite automata (QFAs) have been extensively studied in the literature. In this paper, we define and systematically study quantum B\"uchi automata (QBAs) over infinite words to model the long-term behavior of quantum systems, which…

In this paper, we provide a complete classification for the first-order Goedel logics concerning the property that the formulas admit logically equivalent prenex normal forms. We show that the only first-order Goedel logics that admit such…

Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems for an imperative programming model with discrete…

A variant of the standard notion of branching bisimilarity for processes with discrete relative timing is proposed which is coarser than the standard notion. Using a version of ACP (Algebra of Communicating Processes) with abstraction for…

In the business rules of supply chains, there are concerns around trust, truth, demonstrability and authenticity. These concerns are gathered together under the name ``veracity". In the work for this paper we were originally motivated by…

Behavioural distances of transition systems modelled via coalgebras for endofunctors generalize traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they…

An algorithm for reversible logic synthesis is proposed. The task is, for a given $n$-bit substitution map $P_n: \{0,1\}^n \rightarrow \{0,1\}^n$, to find a sequence of reversible logic gates that implements the map. The gate library…

Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classic versions of LL (ILL and CLL), we obtain two different…

In this paper, we provide a comprehensive, hands-on tutorial on how to apply deductive verification to programs written in OCaml. In particular, we show how one can use the GOSPEL specification language and the Cameleer tool to conduct…

We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a B\"uchi or Parity objective, in finite weighted automata and in one-clock weighted…

Maslov's class $\overline{\text{K}}$ is an expressive fragment of First-Order Logic known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that $\overline{\text{K}}$ has the…

We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of…

We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive…

The complexity of a well-quasi-order (wqo) can be measured through three ordinal invariants: the width as a measure of antichains, height as a measure of chains, and maximal order type as a measure of bad sequences. We study these ordinal…