Provando Teoremas com um Computador

Parece difícil de acreditar mas dá pra fazer isso! Vou fazer isso em linguagem Pascal.
Primeiro passo: codificar as fórmulas matemáticas no computador.
Pensei em duas maneiras de codificar: uma recursiva e outra direta.
Na codificação direta fazemos assim: a fórmula é um array[1..N] of integer, onde N é um número bem grande (depende da memória do seu computador).
Então codificamos os símbolos lógicos ¬[1], ^[2], v[3], →[4], A[5], E[6], =[7], ([8], )[9], xn[10n],l cn[10n+1], fn[10n+2], Pn[10n+3]. xn, cn, fn e Pn são as variáveis, constantes, funcionais e predicados da teoria.
E cada símbolo é substituído pelo número ao lado.
Na forma recursiva, que eu prefiro, faz assim: toda fórmula não atômica é um array[1..11] of integer, onde o primeiro número é um conectivo (representado por um número de 1 a 6, como acima), o terceiro e o quarto são os números dos argumentos (que podem ser fórmulas ou variáveis). Uma fórmula atômica é um array[1..11] of integer onde o primeiro é o número do predicado, e os seguintes os números dos termos. E um termo é um array[1..11] of integer onde o primeiro é o número do funcional, e os seguintes os números dos termos ou variáveis. Pode-se padronizar que variáveis sejam números pares e termos compostos números ímpares, de semelhante modo fórmluas atômicas com números pares.
Depois extende-se isso para conjuntos de fórmulas e termos: um array[1..N,1..11] of integer, onde N é um número muito grande. Esse arranjo é a lista das fórmulas.

Por exemplo, como escrever Ax(x e R→(x²>=0)). Numeramos as fórmulas 2: x²>=0; 4: x e R; 1: x e R→(x²>=0); 3: Ax(x e R→(x²>=0)). Então o array fica assim:
[→,2,4,...]
[>=,x²,0,...]
[A,x,1,...]
[e,x,R,...]

Mais tarde eu ponho como fica o programa...