计算机科学中的逻辑

We investigate self-correcting gossip protocols with errors. In distributed computing, protocols with errors have been widely investigated in temporal epistemic logics. Instead, we propose a dynamic epistemic logic. We show how to correct…

Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification. While automata-based verification scales well when…

We develop a diagrammatic proof system for a fragment of structural semantics inspired by the Greimas semiotic square, using spider diagrams as the underlying formalism. The basic terms are represented as diagrammatic configurations, and…

In this paper, we establish an analogue of Craig Interpolation Property for a many-sorted variant of first-order hybrid logic. We develop a forcing technique that dynamically adds new constants to the underlying signature in a way that…

We present a verifier of quantum programs called AutoQ 2.0. Quantum programs extend quantum circuits (the domain of AutoQ 1.0) by classical control flow constructs, which enable users to describe advanced quantum algorithms in a formal and…

Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how…

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has…

We investigate the eliminability of the absoluteness operator Delta in Goedel logics. While Delta is not definable from the standard connectives and disrupts important proof-theoretic properties, we show that it becomes eliminable at the…

We introduce a novel logic for the specification of context-free hyperproperties, which capture, e.g., the flow of information in security-critical recursive systems. Intuitively, the logic extends visibly pushdown automata by…

Coalition Logic studies what coalitions can enforce. Recent work treats inability as simple non-ability: $\neg\Eff{C}\varphi$. This conflates two distinct configurations -- a coalition unable to force $\varphi$ may still force…

Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one…

Restricted non-deterministic matrices (RNmatrices) impose constraints on the rows of non-deterministic matrices (Nmatrices), filtering out "unsound" rows and retaining only "valid" ones. This yields a more expressive framework than standard…

We present a variation of Maehara's method to construct Craig-Lyndon interpolants for the three-valued propositional logic of here and there (HT), also known as G\"odel's $G_3$, a superintuitionistic logic of importance in logic…

The classifications of temporal and phylogeny constraint languages stand among the most seminal complexity classifications within infinite-domain Constraint Satisfaction Problems (CSPs), yet remain the most mysterious in terms of algorithms…

This paper introduces higher-order (``nested") Kripke models, a generalization of Kripke models that is remarkably close to Kripke's original idea -- both mathematically and conceptually. Standard models are now $0$-ary models, whereas…

We discuss the syntax and semantics of relational Horn logic (RHL) and partial Horn logic (PHL). RHL is an extension of the Datalog programming language that allows introducing and equating variables in conclusions. PHL is a syntactic…

A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are…

A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are…

We present iSMC, the first self-certifying model checker with interactive certification, a certification paradigm based on the theory of interactive proof systems. iSMC is a symbolic BDD-based model checker for arbitrary properties of…

We introduce Backtrackable Inprocessing (BI), a framework that enables applying inprocessing under the current trail at any decision level, at any point during incremental SAT solving. Our approach lifts the long-standing restriction that…