Support more types of logical systems

[nsbgn]

Implement other systems (sequent, ...) and logical families (modal, fragments of first-order, ...).

[nsbgn]

There is a relationship between sequents and tableaux (as used in [Kurokawa 2012] and mentioned in [Fitting 2005, p.21]; see [First-order logic, Smullyan 1994] for the classical case). The signed tableau system in [Renne 2004] corresponds to the sequent system in [Artemov 2001].

It should be possible to specify sequent systems in terms of tableau systems.

We could have a special entry in the YAML where it's specified that system: sequent with base and translation keys to provide the base tableau system and the way to translate from a tableau to a sequent proof.