计算机科学中的逻辑

Interfaces play a central role in determining compatible component compositions by prescribing permissible interactions between a service provider (server) and its consumers (clients). The high degree of concurrency in asynchronous…

We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that…

An alternative proof of the completeness of relational algebra with respect to allowed formulas of first-order logic is presented. The proof relies on the well-known embedding of relational algebra into cylindric algebra, which makes it…

In a recent work of Matteo Mio on compact quantitative equational theories (here compact means that all its consequences are derivable by means of finite proofs) convex algebras on the carrier set [0,1] whose operations are monotone and…

Herbrand schemes are a method to extract Herband disjunctions directly from sequent calculus proofs, without appealing to cut elimination, using a formal grammar known as a higher-order recursion scheme. In this note, we show that the core…

The relationship between intuitionistic or intermediate logics and logic programming has been extensively studied, prominently featuring Pearce's equilibrium logic and Osorio's safe beliefs. Equilibrium logic admits a fixpoint…

We introduce power term polynomial algebra, a representation language for Boolean formulae designed to bridge conjunctive normal form (CNF) and algebraic normal form (ANF). The language is motivated by the tiling mismatch between these…

Axiomatizing covarieties of coalgebras for an endofunctor is less intuitive than axiomatizing varieties of algebras via equations (Dahlqvist and Schmid, 2022). Existing techniques come from coalgebraic modal logic, pattern avoidance…

This paper initially aimed at proposing a proof that quasi-dense logics have f.m.p, but it contains a major flaw, unfixable.

Sandqvist's base-extension semantics for intuitionistic propositional logic defines a support relation parametrised by atomic bases, with validity identified as support in every base. Sandqvist's completeness theorem answers the global…

Neuro-symbolic reasoning increasingly demands frameworks that unite the formal rigor of logic with the interpretability of large language models (LLMs). We introduce an end to end explainability by construction pipeline integrating the…

Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, with axiom schemas of Tarski-Grothendieck set theory. We carry…

Inductive invariants are crucial in model checking, yet generating effective inductive invariants automatically and efficiently remains challenging. A common approach is to iteratively analyze counterexamples to induction (CTIs) and derive…

Verification of programs operating on heap-allocated data structures, for instance lists or trees, poses significant challenges due to the potentially unbounded size of such data structures. We present time-indexed heap invariants, a novel…

Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same network. In existing neural network verifiers, each query is…

We study which classic modal definability and preservation results survive when attention is restricted to finite structures, where many first-order transfer theorems are known to break down. Several semantic characterizations for modal…

We construct witnesses that can be used to derive strategies in fixpoint games and provide proof that the least fixpoint of a function is either above or not below some given bound. We rely on a lattice-theoretical approach, including a…

This article introduces probabilistic disjunctive normal forms (PDNFs) as a framework for representing and reasoning about uncertainty in logical systems. Unlike classical DNFs, PDNFs assign real-valued weights to variables, encoding…

Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve,…

The analysis and control of stochastic dynamical systems rely on probabilistic models such as (continuous-space) Markov decision processes, but large or continuous state spaces make exact analysis intractable and call for principled…