Skip to content

Enhancement Proposals

Olivier Laurent edited this page Apr 28, 2021 · 27 revisions

Cyclic Proofs

  • Goal: dealing with infinite proofs through back edges connecting a proof leaf to an identical sequent met previously during proof construction
  • Interface: drag and drop a turnstile symbol to another sequent which is equal (not up to permutation since permutation is meaningful)

Clone this wiki locally