Traduction Syntaxique

Un mappage mécaniquement spécifié des formules et des preuves d’un langage formel ou système de preuves vers les formules et preuves d’un autre, défini par règles sur la syntaxe (symboles, connecteurs, formation de termes) et destiné à préserver la dérivabilité syntaxique et les propriétés proof‑théoriques associées.