计算机科学中的逻辑

Answer Set Programming (ASP) is a prominent problem-modeling and solving framework, whose solutions are called answer sets. Epistemic logic programs (ELP) extend ASP to reason about all or some answer sets. Solutions to an ELP can be seen…

In this paper we revisit the problem of computing the closure of a set of attributes given a basis of dependencies or implications. This problem is of main interest in logics, in the relational database model, in lattice theory, and in…

For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satisfies the given formula. For non-linear real arithmetic…

Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of…

Hardware accelerators like quantum annealers or neuromorphic chips are capable of finding the ground state of a Hamiltonian. A promising route in utilizing these devices is via methods from automated reasoning: The problem at hand is first…

The framework of cyclic proof systems provides a reasonable proof system for logics with inductive definitions. It also offers an effective automated proof search procedure for such logics without finding induction hypotheses. Recent…

Generalized trees, we call them O-trees, are defined as hierarchical partial orders, i.e., such that the elements larger than any one are linearly ordered. Quasi-trees are, roughly speaking, undirected O-trees. For O-trees and quasi-trees,…

We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable environment. Examples of…

Guarded recursion is a framework allowing for a formalisation of streams in classical programming languages. The latter take their semantics in cartesian closed categories. However, some programming paradigms do not take their semantics in…

Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of assertions, creating a burden for the proof engineer. In this…

This paper presents a new framework for constructing congruence closure of a finite set of ground equations over uninterpreted symbols and interpreted symbols for the group axioms. In this framework, ground equations are flattened into…

Incorrectness Separation Logic (ISL) is a proof system designed to automate verification and detect bugs in programs manipulating heap memories. In this study, we extend ISL to support variable-length array predicates and pointer…

Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders,…

Error: Peer-review process exposed an error in Theorem 1 that, unfourtunately, is not repairable. Idempotent semigroups are always finite. See Green and Rees [1952], Siekmann and Szab\'o [1981] for details Anti-unification is a fundamental…

When evaluating a counterfactual statement, it is often convenient to specify conditions that ought to be kept unchanged. Formally, this can be done by associating to each counterfactual a ceteris paribus set of formulas, specifying the…

Partial incorrectness logic (partial reverse Hoare logic) has recently been introduced as a new Hoare-style logic that over-approximates the weakest pre-conditions of a program and a post-condition. It is expected to verify systems where…

Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification and model checking, driving a need for a trustworthy tool base for analyzing MLTL. In this work, we…

Standpoint linear temporal logic ($SLTL$) is a recently introduced extension of classical linear temporal logic ($LTL$) with standpoint modalities. Intuitively, these modalities allow to express that, from agent $a$'s standpoint, it is…

We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops, (ii) continuous distributions, and (iii) conditioning. To handle…

Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints. These problems often lack a least general solution.…