计算机科学中的逻辑

We introduce semitopology, a generalisation of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that points represent participants in a decentralised system, and open…

We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted in using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. The notion of…

The logic of bunched implication BI provides a framework for reasoning about resource composition and forms the basis for an assertion language of separation logic which is used to reason about software programs. Propositional BI is…

Since the first conference in Marseille in 1982, the International Conference on Logic Programming (ICLP) has been the premier international event for presenting research in logic programming. These proceedings include the Technical…

We introduce a two-sort weighted modal logic for possibilistic reasoning with fuzzy formal contexts. The syntax of the logic includes two types of weighted modal operators corresponding to classical necessity ($\Box$) and sufficiency…

We introduce Open Horn Type Theory (OHTT), an extension of dependent type theory with two primitive judgment forms: coherence and gap, subject to a mutual exclusion law. Unlike classical or intuitionistic negation, gap is not defined via…

We provide a proof of the $n$-ary Beki\v{c} principle, which states that a vectorial fixpoint of size $n$ can be written in terms of nested fixpoints in each coordinate according to lexicographic order. The proof is inductive.

In this note, we give a linear-size translation from formulas of first-order logic into equations of the calculus of relations preserving validity and finite validity. Our translation also gives a linear-size conservative reduction from…

We consider the two-pronged fork frame $F$ and the variety $\mathbf{Eq}(B_F)$ generated by its dual closure algebra $B_F$. We describe the finite projective algebras in $\mathbf{Eq}(B_F)$ and give a purely semantic proof that unification in…

We introduce the general notions of an index and a core of a relation. We postulate a limited form of the axiom of choice -- specifically that all partial equivalence relations have an index -- and explore the consequences of adding the…

This paper presents the development of a software tool that enables the translation of first-order predicate logic with at most three variables into relation algebra. The tool was developed using the Z3 theorem prover, leveraging its…

This work investigates the algorithmic complexity of non-classical logics, focusing on superintuitionistic and modal systems. It is shown that propositional logics are usually polynomial-time reducible to their fragments with at most two…

Hyperproperties are system properties that relate multiple execution traces and commonly occur when specifying information-flow and security policies. Logics like HyperLTL utilize explicit quantification over execution traces to express…

Hyperproperties are system properties that relate multiple execution traces and occur, e.g., when specifying security and information-flow properties. Checking if a hyperproperty is satisfiable has many important applications, such as…

Simplicial models have become a crucial tool for studying distributed computing. These models, however, are only able to account for the knowledge, but not for the beliefs of agents. We present a new semantics for logics of belief. Our…

We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra $\mathbf{A}$ of truth-degrees. More…

We present ReVEAL, a graph-learning-based method for reverse engineering of multiplier architectures to improve algebraic circuit verification techniques. Our framework leverages structural graph features and learning-driven inference to…

A discrete-time linear dynamical system (LDS) is given by an update matrix $M \in \mathbb{R}^{d\times d}$, and has the trajectories $\langle s, Ms, M^2s, \ldots \rangle$ for $s \in \mathbb{R}^d$. Reachability-type decision problems of…

We propose a graphical language that accommodates two monoidal structures: a multiplicative one for pairing and an additional one for branching. In this colored PROP, whether wires in parallel are linked through the multiplicative structure…

In the article ''On the (Non) NP-Hardness of Computing Circuit Complexity'', Murray and Williams imply the PARTITION decision problem is not known to be NP-hard via $2^{n^{o(1)}}$-size AC0 reductions. In this note, we show PARTITION is…