Testigo (asignación que satisface): definición, ejemplo y equivalente en inglés
Un testigo, o asignación que satisface, es una asignación de valores a las variables que hace verdadera una fórmula. Es la evidencia que muestra el motor siempre que un veredicto depende de que exista una sola fila.
Algunas afirmaciones hablan de una fila («hay un caso en que esto se cumple») y otras de todas las filas («esto se cumple en todos los casos»). Un testigo zanja las del primer tipo: se muestra la fila y la afirmación queda establecida. Un contraejemplo zanja del mismo modo la negación de las del segundo tipo. Ambos se escriben como asignaciones, A = FALSE, B = TRUE, y el motor vuelve a evaluar cada uno con su evaluador independiente antes de mostrarlo, así que un testigo en la página se ha comprobado dos veces, con dos piezas de código distintas.
El artefacto de esta página es la tabla de 4 filas de (A OR B) AND NOT A, cuya columna de salida se lee falso, verdadero, falso, falso. La comprobación de satisfacible se cumple con el testigo A = FALSE, B = TRUE: en esa fila A OR B es verdadera y NOT A es verdadera, así que f es verdadera. La comprobación de contradicción se viola con esa misma fila como contraejemplo, porque una fila verdadera basta para refutar «siempre falsa». La de tautología se viola con el contraejemplo A = FALSE, B = FALSE, la fila 0.
Los testigos convierten un veredicto abstracto en un caso de prueba. Un testigo de «esta regla puede conceder acceso» es una entrada que concede acceso, lista para teclearse en una prueba; un testigo de consistencia de premisas es un escenario en que todas las premisas se cumplen a la vez. El término se confunde con el contraejemplo, que refuta en lugar de probar, y con una demostración general, que un testigo nunca es: una fila muestra que algo puede ocurrir, nunca que ocurre siempre.
Ejemplo
f := (A OR B) AND NOT A · salida
Comprobaciones exactas
Tabla de verdad (4 filas)
| # | A | B | f |
|---|---|---|---|
| 0 | FALSO | FALSO | FALSO |
| 1 | FALSO | VERDADERO | VERDADERO |
| 2 | VERDADERO | FALSO | FALSO |
| 3 | VERDADERO | VERDADERO | FALSO |
Lectura en lenguaje claro
Principiantef es verdadero exactamente cuando se cumplen las dos condiciones siguientes:
1. al menos uno entre A y B es verdadero (pueden serlo ambos)
2. A es falso
En todos los demás casos, f es falso.
Sobre los operadores:
- AND (Y) solo es verdadero cuando todas sus partes son verdaderas.
- OR (O) es inclusivo: es verdadero en cuanto al menos una parte es verdadera, también cuando lo son varias.
- NOT (NO) invierte un valor: lo verdadero pasa a ser falso y lo falso, verdadero.
Intermediof es verdadero exactamente cuando se cumplen las dos condiciones siguientes:
1. al menos uno entre A y B es verdadero (pueden serlo ambos)
2. A es falso
En todos los demás casos, f es falso.
Avanzadof es verdadero exactamente cuando se cumplen las dos condiciones siguientes [conjunción ∧]:
1. al menos uno entre A y B es verdadero (pueden serlo ambos) [disyunción inclusiva ∨]
2. A es falso [negación ¬]
En todos los demás casos, f es falso.
Notación formal: (A ∨ B) ∧ ¬A
El error habitual
Leer un testigo como caso típico. A = FALSE, B = TRUE es una fila que hace verdadera (A OR B) AND NOT A; no dice nada de las otras tres filas, en las que la fórmula es falsa. Un testigo prueba la posibilidad, no la frecuencia.
Preguntas
¿Por qué el motor vuelve a evaluar los testigos?
Porque la ruta rápida que encuentra la fila y el evaluador que la comprueba son código distinto, y un testigo solo se muestra si el evaluador coincide en que la fórmula es verdadera en él. Una discrepancia sería un error que informar, no un resultado que mostrar.
Relacionado
Véase también
- Satisfacible: definición, ejemplo y equivalente en inglés
- Contraejemplo: definición, ejemplo y equivalente en inglés
- Contradicción: definición, ejemplo y equivalente en inglés
- Generador de tablas de verdad: cualquier expresión booleana, hasta 12 variables, con columnas intermedias
- Convertir un contraejemplo en una prueba de regresión
- Lección 9: Contraejemplos
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.