Optimización de Intérpretes Formales Ejecutables desarrollados en Sistemas de Demostración de Teoremas de Orden Superior