计算机科学中的逻辑

Rule mining algorithms are one of the fundamental techniques in data mining for disclosing significant patterns in terms of linguistic rules expressed in natural language. In this paper, we revisit the concept of fuzzy implicative rule to…

We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstract semantics of MDPs to a low-level implementation in LLVM…

Three-valued conditional logic (CL) is defined by Guzm\'an and Squier (1990), and based on McCarthy's noncommutative connectives, axiomatises a short-circuit logic (SCL) that defines more identities than three-valued MSCL (Memorising SCL,…

Data-aware modal logics offer a powerful formalism for reasoning about semi-structured queries in languages such as DataGL, XPath, and GQL. In brief, these logics can be viewed as modal systems capable of expressing both reachability…

The dependently-typed lambda calculus LF is often used as a vehicle for formalizing rule-based descriptions of object systems. Proving properties of object systems encoded in this fashion requires reasoning about formulas over LF typing…

We provide a logical characterization of non-deterministic polynomial time defined by BSS machines over semirings via existential second-order logic interpreted in the semiring semantics developed by Gr\"adel and Tannen. Furthermore, we…

Nominal techniques have been praised for their ability to formalize grammars with binding structures closer to their informal developments. At its core, there lies the definition of nominal sets, which capture the notion of name…

This paper investigates the extension of lattice-based logics into modal languages. We observe that such extensions admit multiple approaches, as the interpretation of the necessity operator is not uniquely determined by the underlying…

Representations are essential to mathematically model phenomena, but there are many options available. While each of those options provides useful properties with which to solve problems related to the phenomena in study, comparing results…

Containers represent a wide class of type constructions relevant for functional programming and (co)inductive reasoning. Indexed containers generalize this notion to better fit the scope of dependently typed programming. When interpreting…

This paper introduces a novel anti-unification algorithm for the generalization of variadic structures with binders, designed as a flexible tool for structural code comparison. By combining nominal techniques for handling variable binding…

This volume contains the proceedings of the 20th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2025), which was held in Brasilia, the capital of Brazil, from October 7 to October 8, 2025. The aim of the LSFA series of…

Although they differ in the functionality they offer, low-level systems exhibit certain patterns of design and utilization of computing resources. In this paper, we argue the position that modalities, in the sense of modal logic, should be…

We present a universal construction of Diophantine equations with bounded complexity in Isabelle/HOL. This is a formalization of our own work in number theory. Hilbert's Tenth Problem was answered negatively by Yuri Matiyasevich, who showed…

Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms and synthesize programs. The tactic…

Over more than three decades, the Situation Calculus has established itself as an elegant, powerful, and concise formalism for specifying dynamical domains as well as for reasoning about the effects of actions of those domains both in the…

Safety-critical systems use redundant input units to improve their reliability and fault tolerance. A voting logic is then used to select a reliable input from the redundant sources. A fault detection and isolation rules help in selecting…

This paper undertakes a foundational inquiry into logical inferentialism with particular emphasis on the normative standards it establishes and the implications these pose for classical logic. The central question addressed herein is: 'What…

We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine non-determinism with probabilistic behaviour. The theorem…

The ABC conjecture implies many conjectures and theorems in number theory, including the celebrated Fermat's Last Theorem. Mason-Stothers Theorem is a function field analogue of the ABC conjecture that admits a much more elementary proof…