The talk will report on the first developments towards the implementation of a fully automated program for the extraction of adequate proof-theoretical counterparts for sufficiently expressive logics characterized by way of a finite set of finite-valued truth-tables. Our implementation has been performed in *ML*, and its application gives rise to an *Isabelle* theory formalizing a given finite-valued logic in terms of classic-like two-signed tableau rules. Intended extensions, improvements and refinements of both our algorithm and its implementation will be commented upon. Joint work with D. Mendonça.