63 citations · 134 across the 19 of their papers we have counts for
20 papers
A decision procedure for intuitionistic modal logic IS4 (and IK4)
Marianna Girlando, Roman Kuznets, Sonia Marin +1
In this paper, we show that the two intuitionistic modal logics IS4 and IK4 are decidable. We provide a constructive decision procedure, that, given a formula, produces either a pr…
Interpolation in Proof Theory
Iris van der Giessen, Raheleh Jalali, Roman Kuznets
This chapter provides a comprehensive overview of proof-theoretic methods for establishing interpolation properties across a range of logics, including classical, intuitionistic, m…
Agent Interpolation for Knowledge
Marta Bílková, Wesley Fussner, Roman Kuznets
We define a new type of proof formalism for multi-agent modal logics with S5-type modalities. This novel formalism combines the features of hypersequents to represent S5 modalities…
Bisimulation for Impure Simplicial Complexes
Marta Bílková, Hans van Ditmarsch, Roman Kuznets +1
As an alternative to Kripke models, simplicial complexes are a versatile semantic primitive on which to interpret epistemic logic. Given a set of vertices, a simplicial complex is…
Consistent Update Synthesis via Privatized Beliefs
Thomas Schlögl, Roman Kuznets, Giorgio Cignarale
Kripke models are an effective and widely used tool for representing epistemic attitudes of agents in multi-agent systems, including distributed systems. Dynamic Epistemic Logic (D…
Communication Modalities
Roman Kuznets
Epistemic analysis of distributed systems is one of the biggest successes among applications of logic in computer science. The reason for that is that agents' actions are necessari…
A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
Hans van Ditmarsch, Krisztina Fruzsa, Roman Kuznets +1
We provide an epistemic logical language and semantics for the modeling and analysis of byzantine fault-tolerant multi-agent systems. This not only facilitates reasoning about the…
A priori Belief Updates as a Method for Agent Self-Recovery
Giorgio Cignarale, Roman Kuznets
Standard epistemic logic is concerned with describing agents' epistemic attitudes given the current set of alternatives the agents consider possible. While distributed systems can…
On Two- and Three-valued Semantics for Impure Simplicial Complexes
Hans van Ditmarsch, Roman Kuznets, Rojo Randrianomentsoa
Simplicial complexes are a convenient semantic primitive to reason about processes (agents) communicating with each other in synchronous and asynchronous computation. Impure simpli…
Extensions of K5: Proof Theory and Uniform Lyndon Interpolation
Iris van der Giessen, Raheleh Jalali, Roman Kuznets
We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform L…
Intuitionistic S4 is decidable
Marianna Girlando, Roman Kuznets, Sonia Marin +2
In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years…
Impure Simplicial Complexes: Complete Axiomatization
Rojo Randrianomentsoa, Hans van Ditmarsch, Roman Kuznets
Combinatorial topology is used in distributed computing to model concurrency and asynchrony. The basic structure in combinatorial topology is the simplicial complex, a collection o…
Fire!
Krisztina Fruzsa, Roman Kuznets, Ulrich Schmid
In this paper, we provide an epistemic analysis of a simple variant of the fundamental consistent broadcasting primitive for byzantine fault-tolerant asynchronous distributed syste…
Uniform interpolation via nested sequents and hypersequents
Iris van der Giessen, Raheleh Jalali, Roman Kuznets
A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents,…
Wanted Dead or Alive : Epistemic logic for impure simplicial complexes
Hans van Ditmarsch, Roman Kuznets
We propose a logic of knowledge for impure simplicial complexes. Impure simplicial complexes represent synchronous distributed systems under uncertainty over which processes are st…
The Persistence of False Memory: Brain in a Vat Despite Perfect Clocks
Thomas Schlögl, Ulrich Schmid, Roman Kuznets
Recently, a detailed epistemic reasoning framework for multi-agent systems with byzantine faulty asynchronous agents and possibly unreliable communication was introduced. We have d…
Causality and Epistemic Reasoning in Byzantine Multi-Agent Systems
Roman Kuznets, Laurent Prosperi, Ulrich Schmid +1
Causality is an important concept both for proving impossibility results and for synthesizing efficient protocols in distributed computing. For asynchronous agents communicating ov…
Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi
Roman Kuznets
We have recently presented a general method of proving the fundamental logical properties of Craig and Lyndon Interpolation (IPs) by induction on derivations in a wide class of int…
Grafting Hypersequents onto Nested Sequents
Roman Kuznets, Björn Lellmann
We introduce a new Gentzen-style framework of grafted hypersequents that combines the formalism of nested sequents with that of hypersequents. To illustrate the potential of the fr…
Explicit Evidence Systems with Common Knowledge
Samuel Bucheli, Roman Kuznets, Thomas Studer
Justification logics are epistemic logics that explicitly include justifications for the agents' knowledge. We develop a multi-agent justification logic with evidence terms for ind…