La semántica de sociedades biasertivas abiertas para el sistema de lógica paraconsistente P1, es caracterizada por una herramienta de inferencia visual llamada árboles de forzamiento semántico para sociedades abiertas. 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 sociedad que la refuta está determinada por las marquillas de las hojas en su árbol de forzamiento.