Árboles de forzamiento semántico para el sistema básico con afirmación y negación alternas (2005)
El lenguaje del sistema LB extiende el lenguaje de la lógicaclá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 incompatibilidady 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 asociadoa 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.