计算机科学中的逻辑

The topological semantics of modal logic has been an active area of research ever since their introduction in the 1940s, with attention shifting in recent years from standard unimodal logic to more expressive frameworks. In particular, an…

The property of hyperformalism has proven to be a powerful tool in the analysis of relevant logics, revealing that increasingly weak relevant logics are closed under increasingly strong classes of non-uniform substitutions. In such…

We study the recently introduced intuitionistic monotone modal logic IM. We first provide a semantic characterisation for a family of natural extensions of IM in terms of constructive neighbourhood models. We then present a calculus for IM…

In recent work, an inquisitive first-order modal logic has been proposed to reason about relations of modal dependence, including the notion of global supervenience (functional dependence among the extensions of predicates relative to a…

We introduce inquisitive action logic, InqAL, a multi-agent modal logic for reasoning about action. While traditional approaches focus on what properties of the outcome an agent can force, InqAL also captures what aspects of the outcome an…

Probability logic (PL) extends propositional logic with countably many probability operators, one for each rational number between 0 and 1. The formulas of this logic are interpreted over the class of Markov processes, i.e., structures of…

A logics' property is decidable in a class of logics if there exists an algorithm that decides whether a finitely axiomatizable logic in the class has the property. Many properties are undecidable for bimodal logics but decidable for linear…

Dynamic epistemic logic represents belief change via model transformations induced by epistemic events. Its standard formulation (Baltag, Moss, Solecki, 1998) provides a natural account of belief expansion through the elimination of…

Team semantics is a general framework where formulas are not interpreted with respect to a single point of evaluation, but with respect to sets of such points. Team semantics is used in dependence logic, to reason about dependencies between…

We investigate a new logic that extends Dynamic Epistemic Logic (DEL), by combining standard epistemic modalities for (individual and distributed) propositional knowledge with operators for (conditional) non-propositional knowledge of a…

There are by now various epistemic modal logics with intersection modalities for distributed knowledge and intersection update modalities for dynamic phenomena like agents sharing (all their) information, agents receiving information from…

On the product of two neighborhood frames, three natural neighborhood functions can be defined: the horizontal one assigning to a point (x, y) the set of all supersets of the Cartesian product of U and y, where U is a neighborhood of x; the…

Spatial models are of increasing interest in traditional computer science domains and beyond. Spatial minimisation procedures are crucial for efficient model checking of such models that are often large in size. For the recent notion of…

Counterfactual explanation in abstract argumentation calls for an answer to the what-if query: would the topic argument still be accepted if the status of certain other arguments were changed? Existing approaches are limited to the but-for…

We present a complete machine-checked formalization of Dana Scott's landmark 1972 paper \emph{Continuous Lattices} \textbf{[Sco72]}, carried out in Lean 4 against mathlib and including the March 1972 Milner correction in \textbf{[Sco72]}…

A central goal of language theory is to compare formalisms by understanding their relative expressive power. One challenging question in this direction is the problem of determining the \emph{common fragment} of two formalisms $F_1$ and…

Guarded Kleene Algebra with Tests (GKAT) is a variant of Kleene algebra which allows for reasoning about simple imperative programs, and which features a decision procedure for program equivalence in nearly linear time. In the current…

In this paper we will present neighborhood semantics for non-normal modal extensions of $\clon$, which is a sublogic of {\sf FDE}. Our framework is built upon earlier work on {\sf FDE}-based non-normal modal logics and employs two different…

Polynomial interpretations from function symbols to natural numbers induce a prominent class of monotone algebras and corresponding well-founded orders on terms, used, e.g., for termination analysis and complexity analysis of term rewrite…

In this work, we generalize Kleene's theorem from free single-sorted algebras to free many-sorted algebras. Our main result establishes that, under appropriate finitary assumptions, a language of a given sort in a free many-sorted algebra…