计算机科学中的逻辑

We investigate the data complexity of the satisfiability problem for the very expressive description logic ZOIQ (a.k.a. ALCHb Self reg OIQ) over quasi-forests and establish its NP-completeness. This completes the data complexity landscape…

We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models which form bicategories and not categories, such as those based…

The busy beaver value BB(n) is the maximum number of steps made by any n-state, 2-symbol deterministic halting Turing machine starting on blank tape. The busy beaver function $n \mapsto \text{BB}(n)$ is uncomputable and, from below, only 4…

Ashenhurst-Curtis decomposition (ACD) is a decomposition technique used, in particular, to map combinational logic into lookup tables (LUTs) structures when synthesizing hardware designs. However, available implementations of ACD suffer…

This paper describes the new TPTP format for representing interpretations. It provides a background survey that helped us ensure that the representation format is adequate for different types of interpretations: Tarskian, Herbrand, and…

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F}\,…

Solving Constrained Horn Clauses (CHCs) is a fundamental challenge behind a wide range of verification and analysis tasks. Data-driven approaches show great promise in improving CHC solving without the painstaking manual effort of creating…

Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such…

While deep learning has achieved significant success in various domains, its application to logic circuit design has been limited due to complex constraints and strict feasibility requirement. However, a recent generative deep neural model,…

PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key…

Multiparty session types (MP) are a type discipline for enforcing the structured, deadlock-free communication of concurrent and message-passing programs. Traditional MP have a limited form of choice in which alternative communication…

This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). In APAL we…

We present nested sequent systems for propositional G\"odel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these…

We use a mechanized verification system, PVS, to examine the argument from Anselm's Proslogion Chapter III, the so-called "Modal Ontological Argument." We consider several published formalizations for the argument and show they are all…

The decidability of axiomatic extensions of the modal logic K with modal reduction principles, i.e. axioms of the form $\Diamond^{k} p \rightarrow \Diamond^{n} p$, has remained a long-standing open problem. In this paper, we make…

Game Logic with sabotage ($\mathsf{GL_s}$) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. $\mathsf{GL_s}$ can be used to model…

The main contribution of the present paper is the introduction of a simple yet expressive hybrid-dynamic logic for describing quantum programs. This version of quantum logic can express quantum measurements and unitary evolutions of states…

We study modal separability for fixpoint formulae: given two mutually exclusive fixpoint formulae $\varphi,\varphi'$, decide whether there is a modal formula $\psi$ that separates them, that is, that satisfies…

Analysis of Markov Decision Processes (MDP) is often hindered by state space explosion. Abstraction is a well-established technique in model checking to mitigate this issue. This paper presents a novel lazy abstraction method for MDP…

Most research on formal system design has focused on optimizing various measures of efficiency. However, insufficient attention has been given to the design of systems optimizing resilience, the ability of systems to adapt to unexpected…