• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Articles
  • On structural proof theory of the modal logic K+ extended with infinitary derivations
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
May 25, 2026
HSE Scientists Train Neural Network to 'Hear' Faults in Electric Motors
Researchers at the AI and Digital Science Institute of the HSE Faculty of Computer Science have developed a new method—the Signature-Guided Data Augmentation (SGDA) framework—that achieves 99% accuracy in motor fault detection and 86% accuracy in fault classification. The application of this approach can reduce industrial equipment repair costs, minimise downtime, and improve production safety. The study results have been published in Engineering Applications of Artificial Intelligence.
May 25, 2026
'The Humanities Serve as a Conscience'
Maria Mizernaia studies Soviet literature and the history of book publishing. In this interview for the HSE Young Scientists project, she discusses plans to publish a novel about besieged Leningrad, AI-provoked reflections on what it means to be human, and how novels can help satisfy our dopamine hunger.
May 25, 2026
Is It Possible to Predict a Citys Life Based on the Shape of Its Neighbourhoods?
Is it possible to predict, based on the configuration of streets and buildings, where a café will open or where traffic congestion will occur? Participants in the Spatial Analysis and Modelling of Urban Processes research and study group use open data and machine learning to identify universal patterns. Alexander Sheludkov and Eduard Somov discuss the purpose of comparing cities, the need for new forms of urban statistics, and how open data is transforming approaches to urban studies.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

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

Logic Journal of the IGPL. 2024. P. 1–46.
Shamkanov D. S.

We consider an extension of the modal logic of transitive closure K+ with certain infinitary derivations and present a sequent calculus for this extension, which allows non-well-founded proofs. We establish continuous cut-elimination for the given calculus using fixed-point theorems for contractive mappings. The infinitary derivations mentioned above are well founded and countably branching, while the non-well-founded proofs of the sequent calculus can only be finitely branching. The ordinary derivations in K+⁠, as we show additionally, correspond to the non-well-founded proofs of the calculus that are regular and cut-free. Therefore, in this article, we explore the relationship between deductive systems for K+ with well-founded infinitely branching derivations and (regular) non-well-founded finitely branching proofs.

Language: English
DOI
Keywords: Non-well-founded proofstransitive closureinfinitary derivationscontinuous cut elimination
Similar publications
A realization theorem for the modal logic of transitive closure K+
Shamkanov D. S., Izvestiya. Mathematics 2025 Vol. 89 No. 2 P. 399–421
We present a justification logic corresponding to the modal logic of transitive closure K+ and establish a normal realization theorem relating these two systems. The result is obtained by means of a sequent calculus allowing non-well-founded proofs. ...
Added: November 13, 2024
On structural proof theory of the modal logic K+ extended with infinitary derivations
Shamkanov D. S., / Series arXiv "math". 2023.
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-founded proofs. For the given calculus, we obtain the cut-elimination theorem following the lines of so called continuous cut elimination. Our consideration also covers ordinary proofs of K+ since ...
Added: November 14, 2023
Topological semantics of the predicate modal calculus QGL extended with non-well-founded proofs
Разумный П. М., Shamkanov D. S., , in: SCAN 2023 Semantical and Computational Aspects of Non-Classical Logics: Moscow + Online, June 13–17, 2023. Abstracts.: M.: ., 2023. P. 64–66.
The paper investigates the predicate modal calculus QGL extended with non-well-founded proofs. ...
Added: October 26, 2023
On algebraic and topological semantics of the modal logic of common knowledge S4CI
Shamkanov D. S., Logic Journal of the IGPL 2024 Vol. 32 No. 1 P. 164–179
For the modal logic S4CI, we identify the class of completable S4IC-algebras and prove for them a Stone-type representation theorem. As a consequence, we obtain strong algebraic and topological completeness of the logic S4CI in the case of local semantic consequence relations. In addition, we consider an extension of the logic S4CI with certain infinitary derivations and establish ...
Added: November 30, 2022
Modal logics with transitive closure: Completeness, decidability, filtration
Kikot S., Shapirovsky I., Zolin E., , in: Advances in Modal LogicVol. 13.: College Publications, 2020. P. 369–388.
We give a sufficient condition for Kripke completeness of modal logics that have the transitive closure modality. More precisely, we show that if a modal logic admits what we call definable filtration, then its enrichment with the transitive closure modality (and the corresponding axioms) is Kripke complete; in addition, the resulting logic has the finite ...
Added: December 2, 2020
Cut Elimination for the Weak Modal Grzegorczyk Logic via Non-well-Founded Proofs
Savateev Y., Shamkanov D. S., , in: Logic, Language, Information, and Computation: 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, ProceedingsVol. 11541: Lecture Notes in Computer Science.: Berlin, Heidelberg: Springer, 2019. P. 569–583.
We present a sequent calculus for the weak Grzegorczyk logic 𝖦𝗈 allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs. ...
Added: September 16, 2019
Non-well-founded proofs for the Grzegorczyk modal logic
Yury Savateev, Daniyar Shamkanov, Review of Symbolic Logic 2021 Vol. 14 No. 1 P. 22–50
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 continuous cut-elimination mapping acting on these proofs. As an application, we establish the Lyndon interpolation property for the logic Grz proof-theoretically. ...
Added: February 26, 2018
Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
Savateev Y., Shamkanov D. S., , in: Logic, Language, Information, and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, Proceedings.: Springer, 2017. P. 321–335.
We present a sequent calculus for the modal Grzegorczyk logic ...
Added: September 26, 2017
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit