¿Qué es?
No se ha añadido ninguna twiki todavía.
Algoritmo o método efectivo para poder decidir si una fórmula bien formada de un sistema de lógica es un teorema de dicho sistema, esto es, si puede ser objeto de deducción en una serie finita de pasos sometidos a reglas. La lógica de enunciados dispone de tales procedimientos (las tablas de verdad) pero no la lógica de predicados de primer orden, o la lógica elemental en general, según determina el teorema de Church.