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

This thesis introduces the "method of structural refinement", which serves asa means of transforming the relational semantics of a modal and/or constructivelogic into an 'economical' proof system by connecting two proof-theoreticparadigms: labelled and nested sequent calculi. The formalism of labelledsequents has been successful in that cut-free calculi in possession ofdesirable proof-theoretic properties can be automatically generated for largeclasses of logics. Despite these qualities, labelled systems make use of acomplicated syntax that explicitly incorporates the semantics of the associatedlogic, and such systems typically violate the subformula property to a highdegree. By contrast, nested sequent calculi employ a simpler syntax and adhereto a strict reading of the subformula property, making such systems useful inthe design of automated reasoning algorithms. However, the downside of thenested sequent paradigm is that a general theory concerning the automatedconstruction of such calculi (as in the labelled setting) is essentiallyabsent, meaning that the construction of nested systems and the confirmation oftheir properties is usually done on a case-by-case basis. The refinement methodconnects both paradigms in a fruitful way, by transforming labelled systemsinto nested (or, refined labelled) systems with the properties of the formerpreserved throughout the transformation process.  To demonstrate the method of refinement and some of its applications, weconsider grammar logics, first-order intuitionistic logics, and deontic STITlogics. The introduced refined labelled calculi will be used to provide thefirst proof-search algorithms for deontic STIT logics. Furthermore, we employour refined labelled calculi for grammar logics to show that every logic in theclass possesses the effective Lyndon interpolation property.

Refining Labelled Systems for Modal and Constructive Logics with Applications