计算机科学中的逻辑

Subatomic logic is a recent innovation in structural proof theory where atoms are no longer the smallest entity in a logical formula, but are instead treated as binary connectives. As a consequence, we can give a subatomic proof system for…

We present a formalization, in the theorem prover Lean, of the classification of solvable Lie algebras of dimension at most three over arbitrary fields. Lie algebras are algebraic objects which encode infinitesimal symmetries, and as such…

We introduce two approximate variants of inclusion dependencies and examine the axiomatization and computational complexity of their implication problems. The approximate variants allow for some imperfection in the database and differ in…

We study the model enumeration problem of the function-free, finite domain fragment of first-order logic with two variables ($FO^2$). Specifically, given an $FO^2$ sentence $\Gamma$ and a positive integer $n$, how can one enumerate all the…

This paper introduces a proof calculus for real-analytic differential-algebraic dynamic logic, enabling correct transformations of differential-algebraic equations. Applications include index reductions from differential-algebraic equations…

When validating formal models, sizable effort goes into ensuring two types of properties: safety properties (nothing bad happens) and liveness properties (something good occurs eventually. Event-B supports checking safety properties all…

Property Directed Reachability (\textsc{Pdr}), also known as IC3, is a state-of-the-art model checking algorithm widely used for verifying safety properties. While \textsc{Pdr} is effective in finding inductive invariants, its underlying…

We present the first supermartingale certificate for quantitative $\omega$-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic…

We present HornStr, the first solver for invariant synthesis for Regular Model Checking (RMC) with the specification provided in the SMT-LIB 2.6 theory of strings. It is well-known that invariant synthesis for RMC subsumes various important…

Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose proof automation in ITPs such as Coq and…

Inclusion dependencies form one of the most widely used dependency classes. We extend existing results on the axiomatization and computational complexity of their implication problem to two extended variants. We present an alternative…

Many procedures for SAT-related problems, in particular for those requiring the complete enumeration of satisfying truth assignments, rely their efficiency and effectiveness on the detection of (possibly small) partial assignments…

We introduce a novel approach to studying properties of processes in the {\pi}-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in…

This document serves as a companion to the paper of the same title, wherein we introduce a Gentzen-style sequent calculus for HXPathD. It provides full technical details and proofs from the main paper. As such, it is intended as a reference…

Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability properties, such as: Is there a scheduler resolving the…

The study of theory combination in Satisfiability Modulo Theories (SMT) involves various model theoretic properties (e.g., stable infiniteness, smoothness, etc.). We show that such properties can be partly captured by the natural density of…

Monadic stability and the more general monadic dependence (or NIP) are tameness conditions for classes of logical structures, studied in the 80's in Shelah's classification program in model theory. They recently emerged in algorithmic and…

The chase is a fundamental algorithm with ubiquitous uses in database theory. Given a database and a set of existential rules (aka tuple-generating dependencies), it iteratively extends the database to ensure that the rules are satisfied in…

Ehrenfeucht-Fra\"iss\'e (EF) games are a basic tool in finite model theory for proving definability lower bounds, with many applications in complexity theory and related areas. They have been applied to study various logics, giving insights…

In distributed Cyber-Physical Systems and Internet-of-Things applications, the nodes of the system send measurements to a monitor that checks whether these measurements satisfy given formal specifications. For instance in Urban Air…