Comprobador de equivalencia lógica: dos expresiones, veredicto exacto, contraejemplo
Comprueba si dos expresiones booleanas son lógicamente equivalentes. Si no lo son, la herramienta muestra la primera fila en la que difieren, reproducida en un evaluador independiente.
Pega las dos expresiones (tu versión y la de un compañero, una fórmula y su simplificación, una regla antes y después de una refactorización) y el comprobador hace la pregunta exacta: ¿existe alguna asignación de las entradas compartidas en la que las dos difieran? El motor responde por enumeración exhaustiva hasta veinte entradas y con un solucionador SAT más allá, cruza el resultado y, si existe una asignación que difiere, la reproduce en el evaluador y muestra los dos valores.
La tabla de verdad bajo el veredicto lista las dos expresiones como columnas y resalta cada fila que difiere, así que un desacuerdo no es un único contraejemplo sino el conjunto completo de casos en los que las dos fórmulas no coinciden. Para expresiones equivalentes, la etiqueta dice en cuántas filas corrió la comprobación.
Esta es la herramienta detrás de cada etiqueta «con demostración» de este sitio: el simplificador, el conversor a formas normales, el conversor a compuertas y el mapa de Karnaugh derivan formas nuevas y luego llaman a esta comprobación antes de mostrarlas.
Límites
- Tablas de verdad hasta 12 entradas (4096 filas).
- Mapas de Karnaugh hasta 4 variables efectivas.
- Formas normales hasta 4096 términos; expresiones hasta 20000 caracteres y 64 entradas.
Cómo escribir expresiones
Escribe las entradas como nombres (socio, A, credito_ok) y combínalas con AND, OR, NOT, XOR, -> (implica), <-> (si y solo si), NAND(a, b), NOR(a, b), XNOR(a, b), o los símbolos &&, ||, !, ∧, ∨, ¬, ·, +, ′. También funcionan las formas de mintérminos y maxtérminos: Σm(A, B, C; 1, 3), ΠM(A, B; 0). Precedencia: NOT, luego AND, luego XOR, luego OR, luego ->, luego <->; usa paréntesis para ser explícito. =, ==, ^, &, | y ~ se rechazan con una corrección.
Ejemplo
first := NOT (A AND B) · salidasecond := NOT A AND NOT B · salida
Comprobaciones exactas
Tabla de verdad (4 filas)
| # | A | B | first | second |
|---|---|---|---|---|
| 0 | FALSO | FALSO | VERDADERO | VERDADERO |
| 1 | FALSO | VERDADERO | VERDADERO | FALSO |
| 2 | VERDADERO | FALSO | VERDADERO | FALSO |
| 3 | VERDADERO | VERDADERO | FALSO | FALSO |
Diagrama lógico
Preguntas
Las expresiones usan nombres de variables distintos. ¿Puedo compararlas igualmente?
Solo si los nombres significan lo mismo; el comprobador empareja las entradas por nombre. Renombra un lado para que ambos usen los mismos nombres para las mismas entradas, o la comparación tratará a y A como dos entradas distintas.
¿«Equivalente» es lo mismo que «igual»?
En lógica, equivalente significa que tienen el mismo valor en todas las asignaciones, que es lo que se comprueba. = no es un operador en el lenguaje del motor; el bicondicional <-> sí lo es, y que A <-> B sea una tautología es otra forma de decir que A y B son equivalentes.
Relacionado
Herramientas
- Generador de tablas de verdad: cualquier expresión booleana, hasta 12 variables, con columnas intermedias
- Calculadora y simplificador de álgebra de Boole paso a paso (cada ley nombrada y verificada)
- Solucionador de mapas de Karnaugh: de 2 a 4 variables, agrupaciones, SOP y POS
- Conversor a FNC y FND: formas normales conjuntiva y disyuntiva, mintérminos y maxtérminos
- Conversor a solo NAND o solo NOR con demostración de equivalencia
- Comprobador de validez de argumentos: premisas, conclusión, contraejemplo o demostración
- Generador de circuitos lógicos: de expresión booleana a diagrama de compuertas (SVG)
- De expresión booleana a Python, SQL, SMT-LIB y LaTeX
Herramientas
- Generador de tablas de verdad: cualquier expresión booleana, hasta 12 variables, con columnas intermedias
- Calculadora y simplificador de álgebra de Boole paso a paso (cada ley nombrada y verificada)
- Solucionador de mapas de Karnaugh: de 2 a 4 variables, agrupaciones, SOP y POS
- Conversor a FNC y FND: formas normales conjuntiva y disyuntiva, mintérminos y maxtérminos
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.