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