计算机科学中的逻辑

Partial Markov categories are a recent framework for categorical probability theory that provide an abstract account of partial probabilistic computation with updating semantics. In this article, we discuss two order relations on the…

Probabilistic separation logic offers an approach to reasoning about imperative probabilistic programs in which a separating conjunction is used as a mechanism for expressing independence properties. Crucial to the effectiveness of the…

We examine the relationships between axiomatic and cyclic proof systems for the partial and total versions of Hoare logic and those of its dual, known as reverse Hoare logic (or sometimes incorrectness logic). In the axiomatic proof systems…

Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. Linear logic semantics is typically presented in one of two ways: by associating each formula with the set of…

Recent work by Atserias and Dawar (J. Log. Comp 2019) and Tucker-Foltz (LMCS 2024) has established undefinability results in fixed-point logic with counting (FPC) corresponding to many classical complexity results from the hardness of…

It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems rely on semantical techniques. In this work, we study…

Awodey, later with Newstead, showed how polynomial functors with extra structure (termed ``natural models'') hold within them the categorical semantics for dependent type theory. Their work presented these ideas clearly but ultimately led…

Higher-dimensional automata (HDAs) are models of non-interleaving concurrency for analyzing concurrent systems. There is a rich literature that deals with bisimulations for concurrent systems, and some of them have been extended to HDAs.…

Differentiable logics are a family of quantitative logics originated in the machine learning literature. Because of their origin, differentiable logics often come equipped with analytic properties that guarantee that they are…

Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and such DSLs is a tedious engineering chore. To simplify this…

Deontic logics are formalisms for reasoning over norms, obligations, permissions and prohibitions. Input/Output (I/O) Logics are a particular family of so-called norm-based deontic logics that formalize conditional norms outside of the…

Satisfiability Modulo Theory (SMT) solvers have advanced automated reasoning, solving complex formulas across discrete and continuous domains. Recent progress in propositional model counting motivates extending SMT capabilities toward model…

Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of…

This paper introduces effectful toposes as an extension of the effective topos and investigates their structure relative to Lawvere-Tierney topologies. First, we formulate effectful toposes by lifting the evidenced frame, which is a…

Client-server systems are a computing paradigm in concurrent and distributed systems. We deal with unbounded client-server systems (UCS) where all clients are of the same type, interact with a single server and they may enter and exit the…

This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems. Practically meaningful syntactic restrictions naturally ensure that definable properties…

While large language models (LLMs) have demonstrated impressive capabilities in formal theorem proving, current benchmarks fail to adequately measure library-grounded abstraction -- the ability to reason with high-level interfaces and…

We introduce a new class of automata (which we coin EU-automata) running on infininte trees of arbitrary (finite) arity. We develop and study several algorithms to perform classical operations (union, intersection, complement, projection,…

Cardiovascular disease (CVD) remains one of the leading global health challenges, accounting for more than 19 million deaths worldwide. To address this, several tools that aim to predict CVD risk and support clinical decision making have…

Neural networks (NNs) are pervasive across various domains but often lack interpretability. To address the growing need for explanations, logic-based approaches have been proposed to explain predictions made by NNs, offering correctness…