计算机科学中的逻辑

Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment…

Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. We propose to use $\mu$MALL as a formal theory of arithmetic…

We show that the guarded-negation fragment is, in a precise sense, the smallest extension of the guarded fragment with Craig interpolation. In contrast, we show that full first-order logic is the smallest extension of both the two-variable…

We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a…

We present a collection of results that imply that an endofunctor on a category has a terminal object obtainable as a countable limit of its terminal-coalgebra chain. This holds for finitary endofunctors preserving nonempty binary…

Closure spaces, a generalisation of topological spaces, have shown to be a convenient theoretical framework for spatial model checking. The closure operator of closure spaces and quasi-discrete closure spaces induces a notion of…

Deciding the amalgamation property for a given class of finite structures is an important subroutine in classifying countable finitely homogeneous structures. We study the computational complexity of the amalgamation decision problem for…

We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic…

In this paper, we provide a framework integrating distributed multi-robot systems and temporal epistemic logic. We show that continuous-discrete hybrid systems are compatible with logical models of knowledge already used in distributed…

Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have…

This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle…

Metis is an ordered paramodulation prover built into the Isabelle/HOL proof assistant. It attempts to close the current goal using a given list of lemmas. Typically these lemmas are found by Sledgehammer, a tool that integrates external…

Context: With artificial intelligence (AI) being well established within the daily lives of research communities, we turn our gaze toward formal methods (FM). FM aim to provide sound and verifiable reasoning about problems in computer…

SMT solvers use sophisticated techniques for polynomial (linear or non-linear) integer arithmetic. In contrast, non-polynomial integer arithmetic has mostly been neglected so far. However, in the context of program verification, polynomials…

The study of categories abstracting the structural properties of relations has been extensively developed over the years, resulting in a rich and diverse body of work. A previous paper offered a survey providing a modern and comprehensive…

The past decade has witnessed substantial developments in string solving. Motivated by the complexity of string solving strategies adopted in existing string solvers, we investigate a simple and generic method for solving string…

Symmetries have been exploited successfully within the realms of SAT and QBF to improve solver performance in practical applications and to devise more powerful proof systems. As a first step towards extending these advancements to the…

We study the extension of Presburger arithmetic by the class of sub-polynomial Hardy field functions, and show the majority of these extensions to be undecidable. More precisely, we show that the theory $\mathrm{Th}(\mathbb{Z}; <, +,…

Many software applications rely on concurrent and distributed (micro)services that interact via message-passing and various forms of remote procedure calls (RPC). As these systems organically evolve and grow in scale and complexity, the…

Object-centric process mining investigates the intertwined behavior of multiple objects in business processes. From object-centric event logs, object-centric Petri nets (OCPN) can be discovered to replay the behavior of processes accessing…