Comprobación exhaustiva: definición, ejemplo y equivalente en inglés
Una comprobación exhaustiva evalúa una propiedad en todas las asignaciones de las variables, así que su veredicto es una demostración y no una muestra. El motor ejecuta sus comprobaciones de forma exhaustiva hasta 20 entradas e informa de un recuento de filas junto al resultado.
Exhaustiva significa completa: para n variables se evalúan las 2 elevado a n filas, y una propiedad que se cumple en todas se cumple sin más. Esto solo es posible porque las fórmulas proposicionales tienen un número finito de casos; es lo que separa una demostración por tabla de verdad de las pruebas, donde una muestra que pasa deja abiertos los demás casos. El coste se duplica con cada variable, así que el motor pone el límite en 20 entradas, alrededor de un millón de filas, y más allá recurre a un solucionador SAT, donde el resultado sigue siendo exacto pero se encuentra por búsqueda en lugar de por enumeración.
El artefacto de esta página es (A XOR B) <-> (NOT A <-> B). La comprobación de tautología se cumple, f es verdadera en toda asignación, con un recuento de 4 filas. También se ejecutó el simplificador, que no encontró ninguna ley aplicable; informa de la expresión sin cambios con 4 operadores, con la nota de que no se descartan formas equivalentes más pequeñas. Los dos resultados van juntos a propósito: la comprobación demuestra que la fórmula es una tautología, mientras que el simplificador, que solo reescribe sintaxis, no pudo ver que se reduce a TRUE.
La comprobación exhaustiva es la herramienta adecuada para reglas pequeñas, políticas de acceso y diseños a nivel de compuerta, donde las entradas son pocas y el coste de un caso omitido es alto; es el método que hay detrás de cada veredicto de estas páginas. Su límite es el número exponencial de filas, donde toman el relevo los solucionadores SAT y los métodos simbólicos. El término se confunde con las pruebas minuciosas (una muestra grande sigue siendo una muestra) y con la fuerza bruta en sentido peyorativo; para un millón de filas, enumerar es simplemente el método honesto.
Ejemplo
f := (A XOR B) <-> (NOT A <-> B) · salida
Comprobaciones exactas
Tabla de verdad (4 filas)
| # | A | B | f |
|---|---|---|---|
| 0 | FALSO | FALSO | VERDADERO |
| 1 | FALSO | VERDADERO | VERDADERO |
| 2 | VERDADERO | FALSO | VERDADERO |
| 3 | VERDADERO | VERDADERO | VERDADERO |
Lectura en lenguaje claro
Principiantef es verdadero exactamente cuando las dos condiciones siguientes tienen el mismo valor de verdad (se cumplen ambas o ninguna):
1. exactamente uno entre A y B es verdadero (no ambos)
2. A es falso si y solo si B es verdadero
En todos los demás casos, f es falso.
Sobre los operadores:
- Un bicondicional (↔) es verdadero cuando ambos lados tienen el mismo valor.
- XOR (O exclusivo) es verdadero cuando exactamente una de sus dos partes es verdadera.
- NOT (NO) invierte un valor: lo verdadero pasa a ser falso y lo falso, verdadero.
Intermediof es verdadero exactamente cuando las dos condiciones siguientes tienen el mismo valor de verdad (se cumplen ambas o ninguna):
1. exactamente uno entre A y B es verdadero (no ambos)
2. A es falso si y solo si B es verdadero
En todos los demás casos, f es falso.
Avanzadof es verdadero exactamente cuando las dos condiciones siguientes tienen el mismo valor de verdad (se cumplen ambas o ninguna) [bicondicional ↔]:
1. exactamente uno entre A y B es verdadero (no ambos) [disyunción exclusiva ⊕]
2. A es falso si y solo si B es verdadero [bicondicional ↔]
En todos los demás casos, f es falso.
Notación formal: (A ⊕ B) ↔ (¬A ↔ B)
Simplificación paso a paso
El motor no encontró ninguna ley que acorte esta expresión; ya es tan corta como sus leyes de reescritura permiten.
A XOR B <-> (NOT A <-> B) El error habitual
Esperar que el simplificador diga que una fórmula es una tautología. Aplica leyes de reescritura y se detiene cuando ninguna encaja, como hizo aquí con 4 operadores; la comprobación exhaustiva es la que demuestra la propiedad. La página del error sobre los resultados del simplificador explica por qué las dos herramientas responden preguntas distintas.
Preguntas
¿Qué significa el recuento de filas de un veredicto?
El número de filas que la comprobación evaluó antes de decidir. Para una propiedad que se cumple en todas partes, como aquí, es igual al tamaño de la tabla, 4 filas; para una propiedad violada es el número de filas examinadas hasta el primer contraejemplo, que la comprobación vuelve a evaluar y muestra.
Relacionado
Véase también
- Solucionador SAT: definición, ejemplo y equivalente en inglés
- Tabla de verdad: definición, ejemplo y equivalente en inglés
- Tautología: definición, ejemplo y equivalente en inglés
- «Simplificado» no es «mínimo»: lo que un simplificador puede prometer
- Calculadora y simplificador de álgebra de Boole paso a paso (cada ley nombrada y verificada)
- Un tiempo agotado no es un aprobado: resultados «No determinado»
Glosario
Generado a partir del motor de Tangibool, semántica tangibool-semantics/1, motor 1.0.0, compilación . Cada tabla, mapa, simplificación y veredicto de estas páginas lo calculó el motor de Tangibool al compilar el sitio, y cada afirmación la volvió a comprobar el mismo verificador exacto que usa la app. Los límites se indican donde aplican. © 2026 Foreranger LTD.