计算机科学中的逻辑

We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathematical competitions, such as the International Mathematical…

Verifying graph algorithms has long been considered challenging in separation logic, mainly due to structural sharing between graph subcomponents. We show that these challenges can be effectively addressed by representing graphs as a…

Given an ideal $I$ in a commutative ring $A$, a divided power structure on $I$ is a collection of maps $\{\gamma_n \colon I \to A\}_{n \in \mathbb{N}}$, subject to axioms that imply that it behaves like the family $\{x \mapsto…

Considering patterns as sets of their instances, a difference operator over patterns computes a finite set of two given patterns, which represents the difference between the dividend pattern and the divisor pattern. A complement of a…

Distributed systems can be subject to various kinds of partial failures, therefore building fault-tolerance or failure mitigation mechanisms for distributed systems remains an important domain of research. In this paper, we present a…

This paper investigates the problem of testing clause sets for membership in classes known from literature. In particular, we are interested in classes defined via renaming: Is it possible to rename the predicates in a way such that…

To maximize the information gained from a single execution when verifying a concurrent system, one can derive all concurrency-aware equivalent executions and check them against linear specifications. This paper offers an alternative…

In this paper we investigate the question: 'How can A Foundational Classical Singlesuccedent Sequent Calculus be formulated?' The choice of this particular area of proof-theoretic study is based on a particular ground that is, to formulate…

Shininess and strong politeness are properties related to theory combination procedures. In a paper titled "Many-sorted equivalence of shiny and strongly polite theories", Casal and Rasga proved that for decidable theories, these properties…

A classical approach to studying Markov decision processes (MDPs) is to view them as state transformers. However, MDPs can also be viewed as distribution transformers, where an MDP under a strategy generates a sequence of probability…

We formulate learning guided Automated Theorem Proving as Partial Label Learning, building the first bridge across these fields of research and providing a theoretical framework for dealing with alternative proofs during learning. We use…

Much of the current research and development in the field of automated reasoning builds on the infrastructure provided by the TPTP World. The TPTP language for logical formulae is central to the far-reaching adoption of the TPTP World. This…

Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and…

We introduce semitopologies, a generalisation of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that points are participants in some distributed system, and an open…

Separations among the first order logic ${\cal R}ing(0,+,*)$ of finite residue class rings, its extensions with generalized quantifiers, and in the presence of a built-in order are shown, using algebraic methods from class field theory.…

The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its…

Intuitionistic conditional logic, studied by Weiss, Ciardelli and Liu, and Olkhovikov, aims at providing a constructive analysis of conditional reasoning. In this framework, the would and the might conditional operators are no longer…

This paper enriches preexisting satisfiability tests for unquantified languages, which in turn augment a fragment of Tarski's elementary algebra with unary real functions possessing a continuous first derivative. Two sorts of individual…

We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with…

The Circuit Satisfiability (CSAT) problem, a variant of the Boolean Satisfiability (SAT) problem, plays a critical role in integrated circuit design and verification. However, existing SAT solvers, optimized for Conjunctive Normal Form…