Hotian’sArrow.

(p ∨ q) ∧ (q ∨ r)에서 q는 두 행에 각각 나타납니다. 원 하나로 합쳐 버리면 어느 행의 일부인지 사라집니다. 같은 명제의 축은 공유하되, 등장은 행마다 따로 표시합니다.

p → (q ∧ r)도 ¬p ∨ q와 ¬p ∨ r 두 행으로 그립니다.

p ∨ q ∨ r와 ¬p ∨ ¬q에서 p쌍과 q쌍을 동시에 없애고 r을 얻으면 틀립니다. 예를 들어 p가 참, q, r이 거짓이면 두 전제는 참이지만 r은 거짓입니다.

두 행과 명제 하나를 고르는 방식으로 이 오류를 막습니다. 선택하지 않은 부정·긍정의 원은 그대로 새 행에 포함됩니다.

p ∨ ¬p ∨ q는 항상 참인 행 ⊤입니다. 두 원만 지우고 q를 남기면 안 됩니다. 식을 도해로 바꿀 때는 이 행 전체를 ‘항상 참’으로 정리합니다.

한편 p ∨ p처럼 같은 리터럴이 반복되면 원 하나로 충분합니다.

빈 절 하나는 ⊥, 즉 모순입니다. p 한 행과 ¬p 한 행을 해소하면 이 빈 절을 얻습니다. 도해에서는 빈칸으로 방치하지 않고 반드시 ⊥라고 씁니다.

조건 행이 하나도 없는 판은 ⊤입니다. 추가 제약이 없다는 뜻입니다. 아직 입력하지 않은 편집 화면과도 구별합니다.

p → q와 p → r는 함께 p → (q ∧ r)를 뜻합니다. 이 전제들만으로 q ∧ r이 따라오지는 않습니다. p가 거짓이고 q, r도 거짓인 경우가 허용되기 때문입니다.

여기에 p가 전제로 추가되면 q와 r을 각각 얻을 수 있습니다. 가능하다는 것과 반드시 따라온다는 것을 구별합니다.

(p ∧ q) ∨ r를 단순히 세 원으로 뭉쳐 놓지 않습니다. 분배법칙으로 (p ∨ r) ∧ (q ∨ r)로 바꾼 다음 두 행을 그립니다. 점선이나 우연한 높이에 전체 의미를 맡기지 않습니다.

모든 유한한 고전 명제논리식은 이런 절들의 묶음으로 표현할 수 있습니다. 다만 동치인 식이 반드시 똑같은 그림이 되는 것은 아니며, 전개가 커질 수 있습니다. 실험실의 입력 제한은 이 복잡도를 숨기지 않기 위한 장치입니다.[2]