Procedimiento de prueba

En lógica , y en particular en teoría de la demostración , un procedimiento de demostración para una lógica dada es un método sistemático para producir demostraciones en algún cálculo de demostración de enunciados (demostrables).

Existen varios tipos de cálculos de demostración. Los más populares son la deducción natural , los cálculos de secuencias (es decir, los sistemas de tipo Gentzen ), los sistemas de Hilbert y los diagramas o árboles semánticos . Un procedimiento de demostración dado se centra en un cálculo de demostración específico, pero a menudo puede reformularse para producir demostraciones en otros estilos.

Un procedimiento de demostración para una lógica es completo si produce una demostración para cada enunciado demostrable. Los teoremas de los sistemas lógicos suelen ser recursivamente enumerables , lo que implica la existencia de un procedimiento de demostración completo, pero generalmente muy ineficiente; sin embargo, un procedimiento de demostración solo interesa si es razonablemente eficiente.

Ante una afirmación indemostrable, un procedimiento de prueba completo a veces puede detectar y señalar su indemostrabilidad. En el caso general, donde la demostrabilidad es solo una propiedad semidecidible , esto no es posible y, en su lugar, el procedimiento divergirá (no terminará).

• Demostración automatizada de teoremas
• Complejidad de la prueba
• Sistema deductivo

• Willard Quine 1982 (1950). Métodos de lógica . Harvard Univ. Press.