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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

This paper tackles the problem of formulating and proving the completeness offocused-like proof systems in an automated fashion. Focusing is a discipline onproofs which structures them into phases in order to reduce proof searchnon-determinism. We demonstrate that it is possible to construct a completefocused proof system from a given un-focused proof system if it satisfies someconditions. Our key idea is to generalize the completeness proof based onpermutation lemmas given by Miller and Saurin for the focused linear logicproof system. This is done by building a graph from the rule permutationrelation of a proof system, called permutation graph. We then show that fromthe permutation graph of a given proof system, it is possible to construct acomplete focused proof system, and additionally infer for which formulascontraction is admissible. An implementation for building the permutation graphof a system is provided. We apply our technique to generate the focused proofsystems MALLF, LJF and LKF for linear, intuitionistic and classical logics,respectively.

Towards the Automated Generation of Focused Proof Systems