W引擎 · 翻译指南

以下是编写W脚本的核心语法规则与示例。面向LLM的完整翻译规范请参阅系统提示词文档。

核心概念：事实声明与关系声明

事实声明（→ 开头）
告诉系统"这个命题被设定为真"。只有确定性的真值才能作为事实声明。
→ 下雨   — 确定"下雨"为真
→ ～地湿   — 确定"地湿"为假
→ 下雨 ∧ 刮风   — 确定两者都为真
关系声明（不加 →）
建立命题之间的逻辑关系，不注入任何真值。对关系声明来说，只有"成立与否"，没有"真假"可言。
下雨 → 地湿   — 建立推演通道（同真同假）
A ∨ B   — 建立析取关系（至少一个为真）

语法红线（绝对禁止）

禁止写法原因正确写法
～A → B前件为否定原子A → ～B
～A → ～B前件为否定原子A → B
→ ～～A双重否定禁止→ A 或 → ～A
→ (A ∧ B)事实声明后跟复合命题→ A 和 → B（分两行）
→ (A ∨ B)事实声明后跟复合命题A ∨ B（独立成行，不加→）
→ ∀x(...)事实声明后跟量词量词独立成行，不加→
x = y等词不支持用反对称关系谓词表达
f(x)函数符号不支持改用关系谓词表达

翻译示例

肯定前件
如果下雨地会湿，下雨了，问地湿了吗？
下雨 → 地湿 → 下雨 ? 地湿 SAT?
否定后件
如果下雨地会湿，地没湿，问下雨了吗？
下雨 → 地湿 → ～地湿 ? 下雨 SAT?
三段论验证
所有M是P，所有S是M，验证所有S是P。
∀x(M(x)→P(x)) ∀x(S(x)→M(x)) → S(A) ? P(A) SAT?
关系推理
R是对称关系，已知R(A,B)，验证R(B,A)。
∀x∀y(R(x,y)→R(y,x)) → R(A,B) ? R(B,A) SAT?
可废止推理
所有人都可以借书，但未满12岁不能借。小红10岁，问小红能借书吗？
∀x(人(x)→可借书(x)) ∀x(未满12岁(x)→～可借书(x)) → 人(小红) → 未满12岁(小红) ? 可借书(小红) SAT?

查询格式

用户提问
脚本以 ? 命题 标记查询目标，以 SAT? 结尾。
如需更详细的语法规范，请联系研究者（见Demo网站首页底部）。
面向LLM的完整翻译规范请参阅W引擎系统提示词文档。