计算机科学中的逻辑

In this paper, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the…

Automated deduction seeks to enable machines to reason with mathematical precision and logical completeness. Classical resolution-based systems, such as Prover9, E, and Vampire, rely on binary inference, which inherently limits multi-clause…

We study various notions of dependency in semiring team semantics. Semiring teams are essentially database relations, where each tuple is annotated with some element from a positive semiring. We consider semiring generalizations of several…

This thesis investigates the central role of homomorphism problems (structure-preserving maps) in two complementary domains: database querying over finite, graph-shaped data, and constraint solving over (potentially infinite) structures.…

This paper revisits timed games by building upon the semantics introduced in "The Element of Surprise in Timed Games". We introduce some modifications to this semantics for two primary reasons: firstly, we recognize instances where the…

Real-time cybersecurity and privacy applications require reliable verification methods and system design tools to ensure their correctness. Many of these reactive real-time applications embedded in various infrastructures, such as airports,…

We investigate machine models similar to Turing machines that are augmented by the operations of a first-order structure $\mathcal{R}$, and we show that under weak conditions on $\mathcal{R}$, the complexity class $\text{NP}(\mathcal{R})$…

Quantified Conflict Driven Clause Leaning (QCDCL) is one of the main approaches to solving Quantified Boolean Formulas (QBF). Cube-learning is employed in this approach to ensure that true formulas can be verified. Dependency Schemes help…

Autonomous cyber-physical systems like robots and self-driving cars could greatly benefit from using formal methods to reason reliably about their control decisions. However, before a problem can be solved it needs to be stated. This…

The Ramsey problem $R(3, k)$ seeks to determine the smallest value of $n$ such that any red/blue edge coloring of the complete graph on $n$ vertices must either contain a blue triangle (3-clique) or a red clique of size $k$. Despite its…

Quantum algorithms leverage the use of quantumly-controlled data in order to achieve computational advantage. This implies that the programs use constructs depending on quantum data and not just classical data such as measurement outcomes.…

We show how an effect algebra $\mathcal{X}$ can be regarded as a category, where the morphisms $x \rightarrow y$ are the elements $f$ such that $x \leq f \leq y$. This gives an embedding $\mathbf{EA} \rightarrow \mathbf{Cat}$. The interval…

We describe a framework for maintaining forest algebra representations that are of logarithmic height for unranked trees. Such representations can be computed in O(n) time and updated in O(log(n)) time. The framework is of potential…

We extend the synthetic theories of discrete and Gaussian categorical probability by introducing a diagrammatic calculus for reasoning about hybrid probabilistic models in which continuous random variables, conditioned on discrete ones,…

Strategy logic (SL) is a powerful temporal logic that enables first-class reasoning over strategic behavior in multi-agent systems (MAS). In many MASs, the agents (and their strategies) cannot observe the global state of the system, leading…

Hyperproperties generalize traditional trace properties by relating multiple execution traces rather than reasoning about individual runs in isolation. They provide a unified way to express important requirements such as information flow…

Systems of communicating automata are prominent models for peer-to-peer message-passing over unbounded channels, but in the general scenario, most verification properties are undecidable. To address this issue, two decidable subclasses,…

In this chapter we give a basic overview of known results regarding Craig interpolation for first-order logic as well as for fragments of first-order logic. Our aim is to provide an entry point into the literature on interpolation theorems…

We present a study of unification for rational trees in the context of miniKanren. We give the definition of rational trees, specify the unification algorithm and prove some of its properties. We also introduce a number of heuristic…

Concurrent separation logic with fractional permissions (CSLPerm) provides a promising reasoning system to verify most complex sequential and concurrent fine-grained programs. The logic with strong and weak separating conjunctions offers a…