Árboles de forzamiento semántico para operaciones entre conjuntos

La semántica de valoraciones para la lógica que gobierna las operaciones entre conjuntos es caracterizada por una herramienta de inferencia visual llamada árboles de forzamiento semántico para operaciones entre conjuntos. Dada una fórmula, con esta herramienta se marcan los nodos del árbol asociado a la misma, y se determina si la fórmula es válida o no. En el caso que la fórmula sea inválida, la valoración que la refuta está determinada por las marcas de las hojas en su árbol de forzamiento, además, con esta valoración se construyen los conjuntos que generan el contraejemplo. El análisis de validez realizado con los árboles de forzamiento semántico para operaciones entre conjuntos, evita el paso por los árboles de forzamiento para la lógica de predicados, por lo que las pruebas son más cortas y más intuitivas.