计算机科学中的逻辑

We study the decidability and complexity of equational theories of the existential calculus of relations with transitive closure (ECoR*) and its fragments, where ECoR* is the positive calculus of relations with transitive closure extended…

We develop a unified categorical theory of substructural abstract syntax with variable binding and single-variable (capture-avoiding) substitution. This is done for the gamut of context structural rules given by exchange (linear theory)…

A Markov decision process (MDP) is a state-based dynamical system capable of describing probabilistic behaviour with rewards. In this paper, we view MDPs as coalgebras living in the category of analytic spaces, a very general class of…

We define a new type of proof formalism for multi-agent modal logics with S5-type modalities. This novel formalism combines the features of hypersequents to represent S5 modalities with nested sequents to represent the T-like modality…

Verification is one of the central tasks in circuit and system design. While simulation and emulation are widely used, complete correctness can only be ensured based on formal proof techniques. But these approaches often have very high run…

Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We improve redundancy elimination by introducing a new notion of redundancy, based on partial clauses and redundancy formulas, which is…

The superposition calculus for reasoning in first-order logic with equality relies on simplification orderings on terms. Modern saturation provers use the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) for discovering…

We consider the problem of distributing a centralised transition system to a set of asynchronous agents recognising the same language. Existing solutions are either manual or involve a huge explosion in the number of states from the…

We lift the computability path order and its extensions from plain higher-order rewriting to higher-order rewriting on beta-eta-normal forms where matching modulo beta-eta is employed. The resulting order NCPO is shown to be useful on…

Congruence closure on ground equations is a well-established and efficient algorithm for deciding ground equalities. It constructs an explicit representation of ground equivalence classes based on a given set of input equations, allowing…

Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game…

We propose a systematic study of the so-called flattening operator in team semantics. This operator was first introduced by Hodges in 1997, and has not been studied in more detail since. We begin a systematic study of the expressive power…

Standard Description Logics (DLs) can encode quantitative aspects of an application domain through either number restrictions, which constrain the number of individuals that are in a certain relationship with an individual, or concrete…

We consider the relationship between learnability of a "base class" of functions on a set $X$, and learnability of a class of statistical functions derived from the base class. For example, we refine results showing that learnability of a…

The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those…

A generalization of Scott's information systems~\cite{sco82} is presented that captures exactly all continuous domains. The global consistency predicate in Scott's definition is relativized. Now, for every atomic statement, there is a…

It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula…

Providing explanations for the outputs of artificial neural networks (ANNs) is crucial in many contexts, such as critical systems, data protection laws and handling adversarial examples. Logic-based methods can offer explanations with…

GPU computing is embracing weak memory concurrency for performance improvement. However, compared to CPUs, modern GPUs provide more fine-grained concurrency features such as scopes, have additional properties like divergence, and thereby…

We show that extension variables in (D)QBF can be generalised by conditioning on universal assignments. The benefit of this is that the dependency sets of such conditioned extension variables can be made smaller to allow easier refutations.…