Una disyunción de literales (átomos o sus negaciones) tratada como una sola unidad sintáctica, usada comúnmente en forma normal conjuntiva (FNC) y como objeto básico en procedimientos de prueba basados en resolución y en solveadores SAT.

Principio

Una cláusula codifica la restricción de que al menos uno de sus literales debe ser verdadero; representar fórmulas como conjuntos de cláusulas (FNC) permite la aplicación uniforme de resolución y propagación unitaria.

Demostración

Considere la cláusula (¬P ∨ Q ∨ R) y la cláusula unidad (P). Resolviéndolas se obtiene el resolvente (Q ∨ R). En una refutación por resolución, pasos repetidos de resolución sobre cláusulas pueden derivar la cláusula vacía, indicando insatisfacibilidad.

Aplicación incorrecta

Tratar una cláusula como equivalente a una implicación en contextos donde el alcance de variables o cuantificadores importa ( lógica de primer orden) sin renombrado, o usar resolución a ciegas sobre fórmulas no normalizadas en FNC, lo que puede conducir a resultados incorrectos.

Consecuencia

Ver el conocimiento como un conjunto de cláusulas permite técnicas algorítmicas eficientes (propagación unitaria, watched literals, DPLL/CDCL para SAT y demostración por resolución) y una representación modular de restricciones proposicionales.

Inversión

El punto de vista dual es la conjunción de literales (un cube) o tratar fórmulas completas en lugar de cláusulas normalizadas; volver a la estructura arbitraria de fórmulas puede mejorar la legibilidad pero pierde la uniformidad explotada por los algoritmos de resolución.

Límite

Una cláusula es una forma sintáctica específica (disyunción finita de literales); se aplica en contextos proposicionales y de primer orden (con variables y cuantificadores implícitos) tras normalización y renombrado adecuados, y excluye la estructura booleana anidada arbitraria salvo que se normalice.

Tensión semántica

Existe tensión entre la representación por cláusulas, compacta y eficiente para el cálculo, y las representaciones a nivel de fórmula que preservan con mayor fidelidad la estructura sintáctica y el significado; las cláusulas favorecen la computación, las fórmulas la interpretabilidad humana.

Síntesis

Una cláusula es una unidad sintáctica normalizada —una disyunción finita de literales— usada para expresar restricciones en FNC que resulta especialmente adecuada para resolución y algoritmos SAT, a cambio de una pérdida relativa de riqueza sintáctica.