Traducción Sintáctica

Un mapeo especificado mecánicamente desde fórmulas y pruebas de un lenguaje formal o sistema de pruebas a fórmulas y pruebas de otro, definido por reglas sobre la sintaxis (símbolos, conectivos, formación de términos) y destinado a preservar la derivabilidad sintáctica y propiedades pruebas‑teóricas relacionadas.