01 / 输入公式
一阶谓词逻辑点击填入
支持 ∀ ∃ ¬ ∧ ∨ → ↔、等式、谓词及函数项。也可输入 forall、exists、->、&、|。复杂的量词辖域请显式加括号。
QUINE · GRAPHICAL LOGIC
让变量之间的关系，
成为看得见的线条。
输入一阶逻辑公式，自动生成 Quine 的 bond notation：量词保留，受约束变量变成黑点，并通过弧线连接到所对应的量词。
02 / 连线记法
量词通过曲线与其约束的每一个变量位置连接
QUANTIFICATION BONDS
悬停在量词或黑点上，可高亮对应的全部连线 · 公式过长时可横向滚动
03 / 绑定关系
记号说明
每个 ● 表示一个被量词约束的变量出现；曲线从对应的 ∀ / ∃ 延伸至该位置。同名变量被内层量词重新约束时，连线会自动分组。自由变量仍以字母显示，未使用的量词不会凭空产生连线。