(JH: Draft an overview by answering the following questions)

  • What is a Logika Proof Language Plugin? As part of this, indicate how the presence of the plugin appears to the user, e.g., new justifications available in the proof language

  • What are typical situations in which you might want to create a plugin? What are some example plugins that we have already implemented or what features of Logika proofs are already written as plugins?

  • At a few high level, what must be coded or configured to create the plugin?