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/

Zendy Open

Presents the pdf analysis as premium feature

PDF Analysis

Insights

Presents the summarisation as premium feature

Summarisation

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

The addition of the bounded contraction rules to Full Lambek Calculus with exchange and weakening ( FL ew ) gives rise to serious complications for proof search. For example, adding to FL ew a naive version of these rules brakes cut-admissibility. Although this can be avoided by refining these rules, in this work we show that even “good” proof systems for FL ew plus bounded contraction do not necessarily lead to good implementations. In order to solve this problem, we propose an extension of the lazy splitting methodology to bounded contractions, showing how to transform our focused, cut-free sequent calculus into a terminating theorem prover. Our system is used to show that the decision problem for FL ew with bounded contraction is in EXPTIME .

From Cut-free Calculi to Automated Deduction: The Case of Bounded Contraction