计算机科学中的逻辑

Misdirection can be defined as the intentional action of causing some misrepresentation in an agent, or in a group of agents. Such misrepresentations may result from verbal actions, as in linguistic deception, or from visual actions, as in…

This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes…

Tape diagrams provide a graphical representation for arrows of rig categories, namely categories equipped with two monoidal structures, $\oplus$ and $\otimes$, where $\otimes$ distributes over $\oplus$. However, their applicability is…

Modern cyber-physical systems (CPS) can consist of various networked components and agents interacting and communicating with each other. In the context of spatially distributed CPS, these connections can be dynamically dependent on the…

Logic programs, more specifically, Answer-set programs, can be annotated with probabilities on facts to express uncertainty. We address the problem of propagating weight annotations on facts (eg probabilities) of an ASP to its standard…

We review four areas of theoretical computer science which share technical or philosophical ideas with the work of Belnap on his useful four-valued logic. Perhaps surprisingly, the inspiration by Belnap-Dunn logic is acknowledged only in…

We present a framework for tree-based proof search, called Zippy. Unlike existing proof search tools, Zippy is largely independent of concrete search tree representations, search-algorithms, states and effects. It is designed to create…

This volume contains the post-proceedings of the Fourteenth and the Fifteenth International Workshops on Graph Computation Models (GCM 2023 and 2024). The workshops took place in Leicester, UK on 18th July 2023 and Enschede, the Netherlands…

The Boolean circuit simplification problem involves finding a smaller circuit that computes the same function as a given Boolean circuit. This problem is closely related to several key areas with both theoretical and practical applications,…

Given its ability to analyse stochastic models ranging from discrete and continuous-time Markov chains to Markov decision processes and stochastic games, probabilistic model checking (PMC) is widely used to verify system dependability and…

We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its…

We work with the signed digit representation of abstract real numbers, which roughly is the binary representation enriched by the additional digit -1. The main objective of this paper is an algorithm which takes a sequence of signed digit…

In this note, by integrating ideas concerning terminating tableaux-based procedures in modal logics and finite frame property of intuitionistic modal logic IK, we provide new and simpler decidability proofs for FIK and LIK.

Parameterized systems play a crucial role in the computer field, and their security is of great significance. Formal verification of parameterized protocols is especially challenging due to its "parameterized" feature, which brings…

This short paper proposes to learn models of satisfiability modulo theories (SMT) formulas during solving. Specifically, we focus on infinite models for problems in the logic of linear arithmetic with uninterpreted functions (UFLIA). The…

We introduce a logical framework for reasoning about "uncertain interpretations" and investigate two key applications: a new semantics for implication capturing a kind of "meaning entailment", and a conservative notion of "evidentially…

We establish a framework that allows us to transfer results between some constraint satisfaction problems with infinite templates and promise constraint satisfaction problems. On the one hand, we obtain new algebraic results for…

Many types of formal verification establish properties about abstract high-level program representations, leaving a large gap to programs at runtime. Although gaps can sometimes be narrowed by techniques such as refinement, a verified…

Boolean formulae compactly encode huge, constrained search spaces. Thus, variability-intensive systems are often encoded with Boolean formulae. The search space of a variability-intensive system is usually too large to explore without…

First-order systems of hyperbolic partial differential equations (PDEs) occur ubiquitously throughout computational physics, commonly used in simulations of fluid turbulence, shock waves, electromagnetic interactions, and even general…