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

Due to its practical importance, context-dependent simplification of goals with conditional lemmas has been studied for three decades, mostly under the label of “contextual rewriting”. We present a flexible framework for controlling the recursive relief of conditions by marking formulas in goals and lemmas. Within this framework, by marking goal formulas as forbidden, we can simulate and improve the well-known approaches of contextual rewriting and case rewriting. Furthermore, we develop novel heuristics which may mark goal formulas as mandatory and lemma formulas as obligatory or generous. Our case studies in the field of rewrite-based inductive theorem proving are encouraging.

Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous