activity
20142026
most citedCircular Proofs for Gödel-Löb Logic

29 citations · 39 across the 11 of their papers we have counts for

collaborators

12 papers

math.LO2026

Cyclic proofs in the equational version of Primitive recursive arithmetic

Daniyar Shamkanov

In this brief note, we present a cyclic proof system developed specifically for the equational version of Primitive recursive arithmetic and establish the equivalence of the two sy…

math.LO2025

(Non-)well-founded derivations in the provability logic

Daniyar Shamkanov

We examine cyclic, non-well-founded and well-founded derivations in the provability logic . While allowing cyclic derivations does not change the system, the non-well…

math.LO2025

Fragments of arithmetic and cyclic proofs

Lev D. Beklemishev, Daniyar S. Shamkanov, Ivan N. Smirnov

We present an alternative cyclic proof system for Peano arithmetic that could be simpler than the existing ones and well-adapted both for proof analysis and for automatizing induct…

math.LO2024

A realization theorem for the modal logic of transitive closure

Daniyar Shamkanov

We present a justification logic corresponding to the modal logic of transitive closure and establish a normal realization theorem relating these two systems. The re…

math.LO2023★ 3 cited

On structural proof theory of the modal logic K+ extended with infinitary derivations

Daniyar Shamkanov

We consider an extension of the modal logic of transitive closure K+ with some inifinitary derivations and present a sequent calculus for this extension, which allows non-well-foun…

math.LO2021★ 1 cited

On algebraic and topological semantics of the modal logic of common knowledge S4CI

Daniyar Shamkanov

We investigate algebraic and topological semantics of the modal logic S4CI and obtain strong completeness of the given system in the case of local semantic consequence relations. I…

math.LO2018

Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

Yury Savateev, Daniyar Shamkanov

We present a sequent calculus for the weak Grzegorczyk logic Go allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elim…

math.LO2018

Non-Well-Founded Proofs for the Grzegorczyk Modal Logic

Yury Savateev, Daniyar Shamkanov

We present a sequent calculus for the Grzegorczyk modal logic Grz allowing cyclic and other non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a…

math.LO2017

Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs

Yury Savateev, Daniyar Shamkanov

We present a sequent calculus for the modal Grzegorczyk logic Grz allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-el…

math.LO2016★ 1 cited

Some abstract versions of Gödel's second incompleteness theorem based on non-classical logics

Lev Beklemishev, Daniyar Shamkanov

We study abstract versions of Gödel's second incompleteness theorem and formulate generalizations of Löb's derivability conditions that work for logics weaker than the classical on…

math.LO2014★ 5 cited

Nested Sequents for Provability Logic GLP

Daniyar Shamkanov

We present a proof system for the provability logic GLP in the formalism of nested sequents and prove the cut elimination theorem for it. As an application, we obtain the reduction…

math.LO2014★ 29 cited

Circular Proofs for Gödel-Löb Logic

Daniyar Shamkanov

We present a sequent-style proof system for provability logic GL that admits so-called circular proofs. For these proofs, the graph underlying a proof is not a finite tree but is a…