计算机科学中的逻辑

The Craig interpolation property (CIP) states that an interpolant for an implication exists iff it is valid. The projective Beth definability property (PBDP) states that an explicit definition exists iff a formula stating implicit…

The QSAT problem, which asks to evaluate a quantified Boolean formula (QBF), is of fundamental interest in approximation, counting, decision, and probabilistic complexity and is also considered the prototypical PSPACEcomplete problem. As…

Constant-rate multi-mode systems (MMS) are hybrid systems with finitely many modes and real-valued variables that evolve over continuous time according to mode-specific constant rates. We introduce a variant of linear temporal logic (LTL)…

Our position is that logic programming is not programming in the Horn clause sublogic of classical logic, but programming in a logic of (inductive) definitions. Thus, the similarity between prototypical Prolog programs (e.g., member,…

We give a presentation of Krivine and Parigot's Second-order functional arithmetic in Deduction modulo. Expressing this theory in Deduction modulo sheds light on an original aspect of this theory: the fact that programs are specified, not…

We give a presentation of Simple Type Theory as a clausal rewrite system in Polarized deduction modulo.

The physical Church thesis is a thesis about nature that expresses that all that can be computed by a physical system-a machine-is computable in the sense of computability theory. At a first look, this thesis seems contradictory with the…

Parameterized verification of coverability in broadcast networks with finite state processes has been studied for different types of models and topologies. In this paper, we attempt to develop a theory of broadcast networks in which the…

In recent years, a new class of models for multi-agent epistemic logic has emerged, based on simplicial complexes. Since then, many variants of these simplicial models have been investigated, giving rise to different logics and…

We study the polyregular string-to-string functions, which are certain functions of polynomial output size that can be described using automata and logic. We describe a system of combinators that generates exactly these functions. Unlike…

We consider polyregular functions, which are certain string-to-string functions that have polynomial output size. We prove that a polyregular function has output size $\mathcal O(n^k)$ if and only if it can be defined by an MSO…

We study set systems formed by neighborhoods in graphs of bounded twin-width. We start by proving that such graphs have linear neighborhood complexity, in analogy to previous results concerning graphs from classes with bounded expansion and…

One takes advantage of some basic properties of every homotopic $\lambda$-model (e.g.\ extensional Kan complex) to explore the higher $\beta\eta$-conversions, which would correspond to proofs of equality between terms of a theory of…

The fixed-point logic LREC= was developed by Grohe et al. (CSL 2011) in the quest for a logic to capture all problems decidable in logarithmic space. It extends FO+C, first-order logic with counting, by an operator that formalises a limited…

We present a categorical theory of the composition methods in finite model theory -- a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the…

CHERI-C extends the C programming language by adding hardware capabilities, ensuring a certain degree of memory safety while remaining efficient. Capabilities can also be employed for higher-level security measures, such as software…

We study pseudorandomness and pseudorandom generators from the perspective of logical definability. Building on results from ordinary derandomization and finite model theory, we show that it is possible to deterministically construct, in…

We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike $\lambda$-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names…

We introduce a method to prove that a proof search method is not an instance of another. As an example of application, we show that Polarized resolution modulo, a method that mixes clause selection restrictions and literal selection…

Hintikka and Sandu originally proposed Independence Friendly Logic (IF) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantics of natural language. The logic allows for expressing…