计算机科学中的逻辑

We explore a proof language for intuitionistic multiplicative additive linear logic, incorporating the sup connective that introduces additive pairs with a probabilistic elimination, and sum and scalar products within the proof-terms. We…

In this paper we present a framework for modelling \emph{reward-sensitive bisimulations}, that is, bisimulations that account for quantitative differences such as accumulated rewards. To capture both qualitative and quantitative aspects…

STIT logic is a prominent framework for the analysis of multi-agent choice-making. In the available deontic extensions of STIT, the principle of Ought-implies-Can (OiC) fulfills a central role. However, in the philosophical literature a…

This paper develops an assume-guarantee (AG) framework for the compositional verification of probabilistic automata (PAs) with uncertain transition probabilities. We study parametric probabilistic automata (pPAs), where probabilities are…

This paper develops a novel nested sequent proof-search methodology for intuitionistic tense logics (ITLs), supporting finite counter-model extraction. We introduce a new loop-checking method that detects repeating nested sequents using…

We study a resource-sensitive fragment of the problem of extracting a logical discipline from a class of neural architectures by passing through categorization. The starting point is not a pre-existing logic but a category of zone-labelled…

Boolean satisfiability (SAT) problem, the first problem proven to be NP-complete, has become a fundamental challenge in computational complexity, with widespread applications in optimization and verification across many domains. Despite…

This article is about the formalization of synthetic differential geometry with the Lean proof assistant and the mathematical library mathlib. The main result we prove and formalize is a Taylor theorem for functions of several variables,…

Following Hoare's seminal invention, now called Hoare logic, to reason about correctness of computer programs, we advocate a related but fundamentally different approach to reason about access security of computer programs such as access…

We present Generative Logic (GL), a deterministic architecture that starts from user-supplied axiomatic definitions written in a minimalist Mathematical Programming Language (MPL) and systematically explores a configurable region of their…

Symmetry breaking for graphs and other combinatorial objects is notoriously hard. On the one hand, complete symmetry breaks are exponential in size. On the other hand, current, state-of-the-art, partial symmetry breaks are often considered…

The synthesis of reactive systems aims for the automated construction of strategies for systems that interact with their environment. Whereas the synthesis approach has the potential to change the development of reactive systems…

Usual math sets have special types: countable, compact, open, occasionally Borel, rarely projective, etc. Each such set is described by a single Set Theory formula with parameters unrelated to other formulas. Exotic expressions involving…

Uniform interpolation is the property that, for any formula and set of atoms, there exists the strongest consequence omitting those atoms. It plays a central role in knowledge representation and reasoning tasks such as knowledge update and…

We prove that capability safety admits an exact representation as propositional Datalog evaluation (Datalogprop: the monadic, ground, function-free fragment of first-order logic), enabling the transfer of algorithmic and structural results…

Translating human-written mathematical theorems and proofs from natural language (NL) into formal languages (FLs) like Lean 4 has long been a significant challenge for AI. Most state-of-the-art methods either focus on theorem-only NL-to-FL…

A natural strengthening of an algorithm for the (promise) constraint satisfaction problem is its singleton version: we first fix a variable to an element from its domain, then run the algorithm, and remove the element from the domain if the…

Many first-order equational theories, such as the theory of groups or boolean algebras, can be presented by a smaller set of axioms than the original one. Recent studies showed that a homological approach to equational theories gives us…

We formalize symmetry breaking as a set-covering problem. For the case of breaking symmetries on graphs, a permutation covers a graph if applying it to the graph yields a smaller graph in a given order. Canonical graphs are those that…

We investigate semiring provenance--a successful framework originally defined in the relational database setting--for description logics. In this context, the ontology axioms are annotated with elements of a commutative semiring and these…