##  [Cláusula](/es/node/59904) 

 Definición

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

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

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

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

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

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

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

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

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.