— The aim of the present work is to present a characterization of the Gentzen System G by means of a regulated grammar, according to the Formal Languages Theory. Given a proposition, which is supposed to be a tautology, a grammar will be produced and the generation of the respective language will represent a calculation in G. This language can be interpreted as either, a proof or a counter-example of the given proposition. Mechanization of related tasks is made by means of the functional language