English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Intuitionistic grammar logics fuse constructive and multi-modal reasoningwhile permitting the use of converse modalities, serving as a generalization ofstandard intuitionistic modal logics. In this paper, we provide definitions ofthese logics as well as establish a suitable proof theory thereof. Inparticular, we show how to apply the structural refinement methodology toextract cut-free nested sequent calculi for intuitionistic grammar logics fromtheir semantics. This method proceeds by first transforming the semantics ofthese logics into sound and complete labeled sequent systems, which we provehave favorable proof-theoretic properties such as syntactic cut-elimination. Wethen transform these labeled systems into nested sequent systems via theintroduction of propagation rules and the elimination of structural rules. Ourderived proof systems are then put to use, whereby we prove the conservativityof intuitionistic grammar logics over their modal counterparts, establish thegeneral undecidability of these logics, and recognize a decidable subclass,referred to as "simple" intuitionistic grammar logics.

Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement