计算机科学中的逻辑

Challenges to classical logic have emerged from several sources. According to recent work, the behavior of epistemic modals in natural language motivates weakening classical logic to orthologic, a logic originally discovered by Birkhoff and…

Blockchains use consensus protocols to reach agreement, e.g., on the ordering of transactions. DAG-based consensus protocols are increasingly adopted by blockchain companies to reduce energy consumption and enhance security. These protocols…

The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two. Quantifiers in this logic are used in…

We show that Propositional Dynamic Logic (PDL) has the Craig Interpolation Property. This question has been open for many years. Three proof attempts were published, but later criticized in the literature or retracted. Our proof is based on…

We propose the problem of multi-agent path planning for a generalization of the classic Cops and Robbers game via reactive synthesis. Specifically, through the application of LTLt and Coordination Synthesis, we aim to check whether various…

Extensive research on formal verification of machine learning systems indicates that learning from data alone often fails to capture underlying background knowledge, such as specifications implicitly available in the data. Various neural…

A class of graphs $\mathscr{C}$ is monadically stable if for any unary expansion $\widehat{\mathscr{C}}$ of $\mathscr{C}$, one cannot interpret, in first-order logic, arbitrarily long linear orders in graphs from $\widehat{\mathscr{C}}$. It…

Linear Temporal Logic (LTL) is the de-facto standard temporal logic for system specification, whose foundational properties have been studied for over five decades. Safety and cosafety properties define notable fragments of LTL, where a…

Adhesive and quasiadhesive categories provide a general framework for the study of algebraic graph rewriting systems. In a quasiadhesive category any two regular subobjects have a join which is again a regular subobject. Vice versa, if…

Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras.…

Although reasoning about equations over strings has been extensively studied for several decades, little research has been done for equational reasoning on general clauses over strings. This paper introduces a new superposition calculus…

We show that the problem of whether a query is equivalent to a query of tree-width $k$ is decidable, for the class of Unions of Conjunctive Regular Path Queries with two-way navigation (UC2RPQs). A previous result by Barcel\'o, Romero, and…

In this report, we introduce observation algebras, constructed by considering the downclosed subsets of a coherence space ordered by reverse inclusion. These may be interpreted as specifications of sets of events via some predicates with…

Consistent Hoare, Smyth and Plotkin power domains are introduced and discussed by Yuan and Kou. The consistent algebraic operation $+$ defined by them is a binary partial Scott continuous operation satisfying the requirement: $a+b$ exists…

The present work is devoted to Computability Logic (CoL), the young and volcanic research-project developed by Giorgi Japaridze. Our main goal is to provide the reader with a clear panoramic view of this vast new land, starting from its…

We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic proofs and, by the Curry-Howard correspondence, into the domain of typed functional…

FILO is a java application that decides unifiability for a unification problem formulated in the description logic $\mathcal{FL}_0$. If the problem is unifiable, it presents a user with an example of a solution. FILO joins a family of…

We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for G\"odel-L\"ob provability logic. In particular, we consider Sambin and Valentini's sequent system GLseq, Shamkanov's non-wellfounded…

Large Language Models (LLMs) have demonstrated significant potential in generating mathematical proofs. However, a persistent challenge is that LLMs occasionally make mistakes, while even a minor mistake can invalidate an entire proof.…

We study the verification problem of stochastic systems under signal temporal logic (STL) specifications. We propose a novel approach that enables the verification of the probabilistic satisfaction of STL specifications for nonlinear…