计算机科学中的逻辑

The core challenge in applying abstract interpretation lies in the configuration of abstraction and analysis strategies encoded by a large number of external parameters of static analysis tools. To attain low false-positive rates (i.e.,…

In this paper, we introduce a set representation called polynomial logical zonotopes for performing exact and computationally efficient reachability analysis on logical systems. We prove that through this polynomial-like construction, we…

We introduce a new family of temporal logics designed to finely balance the trade-off between expressivity and complexity. Their key feature is the possibility of defining operators of a new kind that we call transformation operators. Some…

We study the equational theory of the Weihrauch lattice with multiplication, meaning the collection of equations between terms built from variables, the lattice operations $\sqcup$, $\sqcap$, the product $\times$, and the finite…

In this work, we have expounded the communication procedure of quantum systems by means of process algebra. The main objective of our research effort is to formally represent the communication between distributed quantum systems. In this…

The Ho-Zhao problem asks whether any two dcpo's with isomorphic Scott closed set lattices are themselves isomorphic, that is, whether the category $\mathbf{DCPO}$ of dcpo's and Scott-continuous maps is $\Gamma$-faithful. In 2018, Ho,…

We introduce the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) the two-variable fragment…

Causality is the relationship where one event contributes to the production of another, with the cause being partly responsible for the effect and the effect partly dependent on the cause. In this paper, we propose a novel and effective…

We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing…

For a sequence of random structures with $n$-element domains over a relational signature, we define its first order (FO) complexity as a certain subset in the Banach space $\ell^{\infty}/c_0$. The well-known FO zero-one law and FO…

We consider the extension of the two-variable guarded fragment logic with local Presburger quantifiers. These are quantifiers that can express properties such as "the number of incoming blue edges plus twice the number of outgoing red edges…

The author introduced models of linear logic known as ''Interaction Graphs'' which generalise Girard's various geometry of interaction constructions. In this work, we establish how these models essentially rely on a deep connection between…

We provide a general and syntactically-defined family of sequent calculi, called \emph{semi-analytic}, to formalize the informal notion of a "nice" sequent calculus. We show that any sufficiently strong (multimodal) substructural logic with…

We introduce Temporal Ensemble Logic (TEL), a monadic, first-order modal logic for linear-time temporal reasoning. TEL includes primitive temporal constructs such as ``always up to $t$ time later'' ($\Box_t$), ``sometimes before $t$ time in…

Many computational problems in modern society account to probabilistic reasoning, statistics, and combinatorics. A variety of these real-world questions can be solved by representing the question in (Boolean) formulas and associating the…

The development of quantum algorithms and protocols calls for adequate modelling and verification techniques, which requires abstracting and focusing on the basic features of quantum concurrent systems, like CCS and CSP have done for their…

We introduce a sound and complete equational theory capturing equivalence of discrete probabilistic programs, that is, programs extended with primitives for Bernoulli distributions and conditioning, to model distributions over finite sets…

In the realm of smart contract security, transaction malice detection has been able to leverage properties of transaction traces to identify hacks with high accuracy. However, these methods cannot be applied in real-time to revert malicious…

We address the problem of compiling defeasible theories to Datalog$^\neg$ programs. We prove the correctness of this compilation, for the defeasible logic $DL(\partial_{||})$, but the techniques we use apply to many other defeasible logics.…

Consider a binary classification problem solved using a feed-forward artificial neural network (ANN). Let the ANN be composed of a ReLU layer and several linear layers (convolution, sum-pooling, or fully connected). We assume the network…