计算机科学中的逻辑

Alonzo is a practice-oriented classical higher-order version of predicate logic that extends first-order logic and that admits undefined expressions. Named in honor of Alonzo Church, Alonzo is based on Church's type theory, Church's…

Many proof assistants allow the use of features and axioms that increase their expressive power. However, these extensions must be used with care, as some combinations are known to lead to logical inconsistencies. Therefore, proof…

Theta is a verification framework that has participated in the CHC-COMP competition since 2023. While its core approach -- based on transforming constrained Horn clauses (CHCs) into control-flow automata (CFAs) for analysis -- has remained…

We consider sets/relations/computations defined by *Elementary Inference Systems* I, which are obtained from Smullyan's *elementary formal systems* using Gentzen's notation for inference rules, and proof trees for atoms P(t_1,...,t_n),…

We are interested in proving satisfiability of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). We propose to prove satisfiability by building a tree automaton recognizing the Herbrand model of the CHCs. If such an…

We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a…

Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally "centrality", i.e. the property for an effect to commute…

This volume contains the post-proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2025), which took place in Zagreb, Croatia, on July 22, 2025, as affiliated workshop of the 37th International Conference on…

Uniform interpolation property (UIP) is a strengthening of Craig interpolation property. It was first established by Pitts(1992) based on a pure proof-theoretic method. UIP in multi-modal $\mathbf{K_n}$, $\mathbf{KD_n}$ and $\mathbf{KT_n}$…

The linguistic applications of the Lambek calculus suggest its semantics over algebras of formal languages. A straightforward approach to construct such semantics indeed yields a brilliant completeness theorem (Pentus 1995). However,…

The proliferation of decentralized financial (DeFi) systems and smart contracts has underscored the critical need for software correctness. Bugs in such systems can lead to catastrophic financial losses. Formal verification offers a path to…

This paper shows that guarded systems of recursive equations have unique solutions up to strong bisimilarity for any process algebra with a structural operation semantics in the ready simulation format. A similar result holds for simulation…

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…

Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often…

Distribution theory is a cornerstone of the theory of partial differential equations. We report on the progress of formalizing the theory of tempered distributions in the interactive proof assistant Lean, which is the first formalization in…

Two families of denotational models have emerged from the semantic analysis of linear logic: dynamic models, typically presented as game semantics, and static models, typically based on a category of relations. In this paper we introduce a…

Many algorithms are specified with respect to a fixed but unspecified parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key. Our aim is…

This volume contains the proceedings of EXPRESS/SOS 2025: the Combined 32nd International Workshop on Expressiveness in Concurrency and the 22nd Workshop on Structural Operational Semantics, which was held in Aarhus, Denmark, as an…

Possibilistic computation tree Logic (PoCTL) is one kind of branching temporal logic combined with uncertain information in possibility theory, which was introduced in order to cope with the systematic verification on systems with uncertain…

In this article we propose an extension to the typed natural deduction calculus TNDPQ to model verification of counterfactual fairness in probabilistic classifiers. This is obtained formulating specific structural conditions for causal…