Função que conta o número de parênteses.
PAR[@]= 0, se @ é variável proposicional
PAR[Falso]=0
PAR[~A]=PAR[A]
PAR[A!B]=PAR[A]+PAR[B]+2
obs: !:= conjunção, disjunção, implicação e bi-implicação
G: PROP-->N
Função que conta o número de operadores.
G[@]= 0, se @ é variável proposicional
G[Falso]=0
G[~A]=G[A]+1
PAR[(A!B)]=PAR[A]+PAR[B]+1
RANK: PROP-->N
Função que mede a profundidade da árvore de formação
RANK[@]= 0, se @ é variável proposicional
RANK[Falso]=0
RANK[~A]=RANK[A]+1
RANK[(A!B)]=MAX[RANK[A], RANK[B]]+1
NI: PROP-->N
Função que mede o número de implicações
NI[@]= 0, se @ é variável proposicional
NI[Falso]=0
NI[~A]=NI[A]
NI[(A&B)]=NI[A]+NI[B]
NI[(AvB)]=NI[A]+NI[B]
NI[(A-->B)]=NI[A]+NI[B]+1
NI[(A<-->B)]=NI[A]+NI[B]
POL: PROP-->PROPpol
Função que estabelece a relação entre a nossa notação e a notação polonesa
POL[@]=@, se @ é variável proposicional
NI[Falso]=Falso
NI[~A]=N POL[A]
NI[(A&B)]=K POL[A]POL[B]
NI[(AvB)]=A POL[A]POL[B]
NI[(A-->B)]=C POL[A]POL[B]
NI[(A<-->B)]=E POL[A]POL[B]
SUB: PROP-->Conjuntos de fórmulas
Função que indica o conjunto de subfórmulas de A
SUB[@]={@}
SUB[Falso]={Falso}
SUB[~A]=SUB[A] U {~A}
SUB[(A!B)]=SUB[A] U SUB[B] U {A!B}
.
