计算机科学中的逻辑

This volume contains the proceedings of the 9th Working Formal Methods Symposium, which was held at the Alexandru Ioan Cuza University, Ia\c{s}i, Romania on September 17-19, 2025.

Tabular intermediate logics are intermediate logics characterized by finite posets treated as Kripke frames. For a poset $\mathbb{P}$, let $L(\mathbb{P})$ denote the corresponding tabular intermediate logic. We investigate the complexity of…

The unification algorithm has long been a target for program synthesis research, but a fully automatic derivation remains a research goal. In deductive program synthesis, computer programming is phrased as a task in theorem proving; a…

Despite its prevalence, in many domains, OWL is not expressive enough to define ontology classes. In this paper, we present an approach that allows to use monadic second-order formalisations for ontology classification. As a case study, we…

Satisfiability Modulo Linear Integer Arithmetic, SMT(LIA) for short, is pivotal across various critical domains. Previous research has primarily focused on SMT solving techniques. However, in practical applications such as software and…

Dynamic techniques are a scalable and effective way to analyze concurrent programs. Instead of analyzing all behaviors of a program, these techniques detect errors by focusing on a single program execution. Often a crucial step in these…

This paper extends the literature on the strict-tolerant logical approach by applying its methods to intuitionistic and minimal logic. In short, the strict-tolerant approach modifies the usual notion of logical consequence by stipulating…

Temporal reasoning in dynamic, data-intensive environments increasingly demands expressive yet tractable logical frameworks. Traditional approaches often rely on negation to express absence or contradiction. In such contexts,…

Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods…

We study the Guarded Fragment with Regular Guards (RGF), which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many…

In this paper we investigate the complexity-theoretical aspects of cyclic and non-wellfounded proofs in the context of parsimonious logic, a variant of linear logic where the exponential modality ! is interpreted as a constructor for…

Coalition Logic is an important logic in logical studies of strategic reasoning, whose models are concurrent game models. In this paper, first, we systematically discuss three assumptions of concurrent game models and argue that they are…

The fundamental building blocks of the Bitcoin lightning network are bidirectional payment channels. We describe an extension of payment channels in the Proofgold network which allow the two parties to bet on whether a proposition will be…

Proofgold is a blockchain that supports formalized mathematics alongside standard cryptocurrency functionality. It incorporates logical constructs into the blockchain, including declarations of formal theories, definitions, propositions and…

We use automated theorem provers to significantly shorten a formal development in higher order set theory. The development includes many standard theorems such as the fundamental theorem of arithmetic and irrationality of square root of…

While modal extensions of decidable fragments of first-order logic are usually undecidable, their monodic counterparts, in which formulas in the scope of modal operators have at most one free variable, are typically decidable. This only…

We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be…

Trustworthy AI requires reasoning systems that are not only powerful but also transparent and reliable. Automated Theorem Proving (ATP) is central to formal reasoning, yet classical binary resolution remains limited, as each step involves…

This paper shows how to use Lee, Jones and Ben Amram's size-change principle to check correctness of arbitrary recursive definitions in an ML / Haskell like programming language with inductive and coinductive types. Naively using the…

Aczel-Mendler bisimulations are a coalgebraic extension of a variety of computational relations between systems. It is usual to assume that the underlying category satisfies some form of the axiom of choice, so that the collection of…