Make a typeclass for Provers

[nsbgn]

Right now, a Tableau is the only proof system that is implemented. However, it would be pleasing to make proof systems more general by adding a typeclass. This would clean up the I/O code, too, since there can be a single I/O function for all decision algorithms.

class (ProofSystem ext system, LaTeX proof, Plain proof) => Prover system 
proof where
    decide :: system -> F.Formula ext -> proof
    analyse :: system -> F.Formula ext -> PP.Doc
    deserialise :: Y.Value -> system