arXiv subjects

Ekaterina Piotrovskaya

Publications and source records attributed to Ekaterina Piotrovskaya.

4 recordsLinked to original sources

arXiv2026

From Phase Semantics to Base-extension Semantics (and back)

Linear logic admits a wide range of semantic presentations reflecting its resource-sensitive notion of consequence. One well-known example is phase semantics: an algebraic semantics in which formulas are interpreted in phase models, consisting of a phase space formed by a commutative monoid and a fixed subset, with respect to which an orthogonality relation is defined, and a valuation. A rather different and much more recent approach is given by base-extension semantics, which defines validity by inductively extending a provability relation on a base -- a set of inference rules over atomic propositions. We establish an equivalence between the two semantics by first defining bidirectional maps between bases and phase models, and then constructing an isomorphism between a phase model (resp. base) and its image under the composition of these maps. As a further contribution, we define the base-extension semantics clauses for the exponentials of linear logic.

cs.LO↗

arXiv2026

A Proof-Theoretic Approach to the Semantics of Classical Linear Logic

Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. Linear logic semantics is typically presented in one of two ways: by associating each formula with the set of all contexts that can be used to prove it (e.g. phase semantics) or by assigning meaning directly to proofs (e.g. coherence spaces). This work proposes a different perspective on assigning meaning to proofs by adopting a proof-theoretic perspective. More specifically, we employ base-extension semantics (BeS) to characterise proofs through the notion of base support. Recent developments have shown that BeS is powerful enough to capture proof-theoretic notions in structurally rich logics such as intuitionistic linear logic. In this paper, we extend this framework to the classical case, presenting a proof-theoretic approach to the semantics of the multiplicative-additive fragment of linear logic (MALL).

cs.LO↗

arXiv2025

A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report)

We define base-extension semantics (Bes) using atomic systems based on sequent calculus rather than natural deduction. While traditional Bes aligns naturally with intuitionistic logic due to its constructive foundations, we show that sequent calculi with multiple conclusions yield a Bes framework more suited to classical semantics. The harmony in classical sequents leads to straightforward semantic clauses derived solely from right introduction rules. This framework enables a Sandqvist-style completeness proof that extracts a sequent calculus proof from any valid semantic consequence. Moreover, we show that the inclusion or omission of atomic cut rules meaningfully affects the semantics, yet completeness holds in both cases.

cs.LO↗

arXiv2024

Learning Closed Signal Flow Graphs

We develop a learning algorithm for closed signal flow graphs - a graphical model of signal transducers. The algorithm relies on the correspondence between closed signal flow graphs and weighted finite automata on a singleton alphabet. We demonstrate that this procedure results in a genuine reduction of complexity: our algorithm fares better than existing learning algorithms for weighted automata restricted to the case of a singleton alphabet.

cs.LO↗