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

Reachability Logic is a formalism that can be used, among others, forexpressing partial-correctness properties of transition systems. In this paperwe present three proof systems for this formalism, all of which are sound andcomplete and inherit the coinductive nature of the logic. The proof systemsdiffer, however, in several aspects. First, they use induction and coinductionin different proportions. The second aspect regards compositionality, broadlymeaning their ability to prove simpler formulas on smaller systems, and toreuse those formulas as lemmas for more complex formulas on larger systems. Thethird aspect is the difficulty of their soundness proofs. We show that the moreinduction a proof system uses, and the more specialised is its use ofcoinduction (with respect to our problem domain), the more compositional theproof system is, but the more difficult its soundness proof becomes. We alsobriefly present mechanisations of these results in the Isabelle/HOL and Coqproof assistants.

(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic