计算机科学中的逻辑

{log} (read 'setlog') was born as a Constraint Logic Programming (CLP) language where sets and binary relations are first-class citizens, thus fostering set programming. Internally, {log} is a constraint satisfiability solver implementing…

We present a choreographic framework for modelling and analysing concurrent probabilistic systems based on the PRISM model-checker. This is achieved through the development of a choreography language, which is a specification language that…

We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate…

We show that the Skolem Problem is decidable in finitely generated commutative rings of positive characteristic. More precisely, we show that there exists an algorithm which, given a finite presentation of a (unitary) commutative ring…

The operations to be performed by a quantum computer are almost invariably given in the form of a quantum circuit. In the final stage of compilation, a quantum circuit must be translated into the input signals accepted by the quantum…

We prove that the equational theory of the positive calculus of relations with transitive closure (PCoR*) is EXPSPACE-complete. Here, PCoR* terms consist of the following standard operators on binary relations: identity, empty,…

Whether LLMs can reason or write software is widely debated, but whether they can write software that itself reasons is largely unexplored. We present a case study in which an LLM coding agent builds a complete DPLL(T)-style SMT solver for…

This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability…

Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles…

The verification of asynchronous software components poses significant challenges due to the way components interleave and exchange input/output data concurrently. Compositional strategies aim to address this by separating the task of…

Previous work has axiomatised the cardinality operation in relation algebras, which counts the number of edges of an unweighted graph. We generalise the cardinality axioms to Stone relation algebras, which model weighted graphs, and study…

We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we generalize the technique to other categories, and we allow for…

Automatic structures are first-order structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular languages that the first-order theory of an automatic structure…

In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as…

Metric Temporal Logic (MTL) is a popular formalism to specify temporal patterns with timing constraints over the behavior of cyber-physical systems with application areas ranging in property-based testing, robotics, optimization, and…

The Central Limit Theorem (CLT) establishes that sufficiently large sequences of independent and identically distributed random variables converge in probability to a normal distribution. This makes the CLT a fundamental building block of…

For computation, there existed Turing machine and later-matured automata theory. For low-level parallel computation, there existed variants of Turing machine, such as two-tapes Turing machine and multi-tapes Turing machine. In the…

In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proof scripts since they enable rapid exploration…

The automated generation of exercises may substantially reduce the time educators devote to manual exercise design. A major obstacle to the integration of such automation into teaching practice, however, lies in the ability to control the…

This paper introduces sketch-oriented databases, a categorical framework that encodes database paradigms as finite-limit sketches and individual databases and schemas as set-valued models. It illustrates the formalism through graph-oriented…