Prueba formal

En lógica, una derivación formal (o prueba formal) es una secuencia finita de sentencias donde cada sentencia puede ser un axioma o puede ser obtenida como consecuencia directa de las sentencias anteriores en la secuencia utilizándose una regla de inferencia. La última frase siguiente es un teorema del sistema formal. La noción del teorema no es efectiva en general, porque no puede haber un método mediante el cual siempre podemos encontrar una derivación de una resolución dictada o determinar que no hay derivación. El concepto de deducción es una generalización del concepto de derivación.

El teorema es una consecuencia sintáctica de todas las fórmulas bien formadas (fbf) precedidas en la derivación. Para una parte fbf de una unión, ella debe ser el resultado de aplicar una regla de sistema deductivo de cualquier sistema formal previa en fbfs siguiente derivación.

Las derivaciones formales muchas veces se construye con la ayuda de ordenadores a través de la demostración interactiva de teoremas. Resulta interesante notar que estas derivaciones pueden ser conferidas automáticamente con el uso del ordenador. Conferir derivaciones formales suele ser una tarea trivial, mientras que encontrar tales derivaciones (demostración automática de teoremas) suele ser bastante difícil.