ÁRBOLES DE FORZAMIENTO SEMÁNTICO PARA EL SISTEMA BÁSICO CON AFIRMACIÓN Y NEGACIÓN ALTERNAS

El lenguaje del sistema LB extiende el lenguaje de la lógica

clásica al incluir operadores para las nociones de afirmación alterna (en contraste con la afirmación usual o afirmación clásica), negación alterna (en contraste con la negación clásica), y también operadores de incompatibilidad

y determinabilidad entre parejas de operadores: negación alterna versus afirmación alterna, negación alterna versus afirmación clásica y afirmación alterna versus negación clásica. El sistema está caracterizado por una herramienta de inferencia visual llamada árboles de forzamiento semántico. Con esta herramienta se marcan los nodos del árbol asociado

a una fórmula dada, y con base en estas marcas se determina si la fórmula es válida o no. En caso de invalidez, la valuación que refuta la validez de la fórmula está determina por las marcas en su árbol de forzamiento.