본 논문은 선형 부등식에 계수 모달 연산자가 나타나는 모달 논리를 제안합니다. 각 공식을 동등한 그래프 신경망(GNN)으로 변환할 수 있음을 보이고, 광범위한 GNN 클래스를 공식으로 효율적으로 변환할 수 있음을 보임으로써 GNN의 논리적 표현력에 대한 기존 연구를 크게 개선합니다. 또한 만족 가능성 문제가 PSPACE-완전함을 증명합니다. 이러한 결과는 GNN 및 그 특성에 대한 추론에 표준 논리적 방법을 사용하는 것, 특히 GNN 쿼리, 동등성 확인 등의 응용 분야에서의 약속을 함께 제시하며, 이러한 자연스러운 문제가 다항 공간에서 해결될 수 있음을 증명합니다.