Regla de inferencia

También se llaman reglas de transformación o de producción. Una regla de inferencia es una regla explícita para producir un teorema a partir de otro(s) teorema(s) dado(s). Son funciones que relacionan teoremas con teoremas. En los sistemas formales las reglas de inferencia son de naturaleza formal (esto es, sintáctica), y operan sin referencia a los significados de las fórmulas que manipulan. Se estudian multitud de reglas de inferencia, como por ejemplo el Modus Ponens o el Modus Tollens. (Véase derivación, función, prueba, teorema).