En lógica , y en particular teoría de la prueba , un procedimiento de prueba para una lógica dada es un método sistemático para producir pruebas en algún cálculo de prueba de enunciados (demostrables).
Tipos de cálculos de prueba utilizados
Hay varios tipos de cálculos de prueba. Los más populares son la deducción natural , los cálculos secuenciales (es decir, los sistemas de tipo Gentzen ), los sistemas de Hilbert y los cuadros o árboles semánticos . Un procedimiento de prueba dado tendrá como objetivo un cálculo de prueba específico, pero a menudo se puede reformular para producir pruebas en otros estilos de prueba.
Lo completo
Un procedimiento de prueba para una lógica está completo si produce una prueba para cada enunciado demostrable. Los teoremas de los sistemas lógicos son típicamente enumerables de forma recursiva , lo que implica la existencia de un procedimiento de prueba completo pero extremadamente ineficaz; sin embargo, un procedimiento de prueba solo es de interés si es razonablemente eficiente.
Frente a una afirmación indemostrable, un procedimiento de prueba completo a veces puede tener éxito en detectar y señalar su indemostrabilidad. En el caso general, donde la demostrabilidad es una propiedad semidecidable , esto no es posible y, en cambio, el procedimiento divergerá (no terminará).
Ver también
Referencias
- W. Quine 1982 (1950). Métodos de lógica . Universidad de Harvard. Prensa.