(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?