计算机科学中的逻辑

PECR is a formal system designed to explore the properties of computability of programs on a real-world computer. As such PECR incorporates the finite resources of the machine upon which a program is to be executed. The main features of the…

Distributive laws are important for algebraic reasoning in arithmetic and logic. They are equally important for algebraic reasoning about concurrent programs. In existing theories such as Concurrent Kleene Algebra, only partial correctness…

We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant for schematic first-order logic and its library based on…

Payroll management is a critical business task that is subject to a large number of rules, which vary widely between companies, sectors, and countries. Moreover, the rules are often complex and change regularly. Therefore, payroll…

This paper presents an up-to-date and refined version of the SCL calculus for first-order logic without equality. The refinement mainly consists of the following two parts: First, we incorporate a stronger notion of regularity into…

A short essay presenting the State-Effect Interpretation of natural deduction rules as an explanatory framework for recent developments in proof-theoretic semantics.

We give complete presentations for the dagger-compact props of affine Lagrangian and coisotropic relations over an arbitrary field. This provides a unified family of graphical languages for both affinely constrained classical mechanical…

Probabilistic model checking can provide formal guarantees on the behavior of stochastic models relating to a wide range of quantitative properties, such as runtime, energy consumption or cost. But decision making is typically with respect…

This paper shows the initial stages of development, from first principles, of a formal logic to characterise and then explore issues in a broadly defined idea of Veracity, which includes properties of demonstrability, truth, trust and…

This note generalizes factorization for formulas with multiplicities and conjectures that the connection method along with this feature is computationally as powerful as resolution, also seen from a complexity point of view.

The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was…

Place bisimilarity $\sim_p$ is a behavioral equivalence for finite Petri nets, originally proposed in \cite{ABS91}, that, differently from all the other behavioral relations proposed so far, is not defined over the markings of a finite net,…

The $\mathrm{Caus}[-]$ construction takes a base category of ``raw materials'' and builds a category of higher order causal processes, that is a category whose types encode causal (a.k.a. signalling) constraints between collections of…

In this paper we propose a language for conveniently defining a wide range of execution strategies for real-time rewrite theories, and provide Maude-strategy-implemented versions of most Real-Time Maude analysis methods, albeit with…

In this dissertation we describe two contributions to the state of the art in reasoning about liveness and safety, respectively. Programs for multiprocessor machines commonly perform busy waiting for synchronization. We propose the first…

Separation logic's compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges -- many programs display computational effects and, orthogonally,…

RoboChart is a core notation in the RoboStar framework which brings modern modelling and formal verification technologies into software engineering for robotics. It is a timed and probabilistic domain-specific language for robotics and…

Information leakage can have dramatic consequences on the security of real-time systems. Timing leaks occur when an attacker is able to infer private behavior depending on timing information. In this work, we propose a definition of…

We investigate intuitionistic modal logics with locally interpreted $\square$ and $\lozenge$. The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization…

The tool mpbn offers a Python programming interface for an easy interactive editing of Boolean networks and the efficient computation of elementary properties of their dynamics, including fixed points, trap spaces, and reachability…