W引擎 · 翻译指南
以下是W脚本的常用语法规则与示例。条件句按五类目标形式翻译；自然语言输入（如"下雨，地湿吗？"）由确定性翻译器自动拆分为规则与查询，无需手动书写脚本。面向LLM的完整翻译规范请参阅系统提示词文档。
1. 事实声明
陈述一个事实，用 → 开头，后跟原子公式。
自然语言：下雨了。
→ Rain
2-1. 充分条件（第①类）→ A → B
如果A那么B / 只要A就B / 一旦A就B / 因为A所以B / 既然A就B / 隐式"A，就B"。规则独立成行，不加 → 前缀。
自然语言：如果下雨，地会湿。
下雨 → 地湿
2-2. 必要条件（第②类）→ B → A
"只有A才B"表达B以A为必要条件，推演方向是 B → A（而非 A → B）。"不A就不B"经等价转换（不A→不B ⟺ B→A）亦归此类。
自然语言：只有努力，才能成功。
成功 → 努力
自然语言：不努力就不成功。
成功 → 努力
2-3. 否定后件（第③类）→ A → ～B
"除非A否则B"= 不A→B ⟺ A→～B；"如果不A那么B"同样归此类；"A不一定B"→ A → ～B。
自然语言：除非下雨，否则出门。
下雨 → ～出门
自然语言：下雨不一定地湿。
下雨 → ～地湿
2-4. 否定前件反写（第④类）→ B → ～A
"不A是B的前提"= B以"不A"为必要条件 → B → ～A；"有B则无A"→ B → ～A；"要B就得放弃A"同此。
自然语言：不熬夜是健康的前提。
健康 → ～熬夜
自然语言：有雾则无航班。
雾 → ～航班
2-5. 充要条件（第⑤类）→ A → B 且 B → A
"A当且仅当B"生成双向两条规则（多通道安全：不能保证知识库只有一条以B为后件的规则）。
自然语言：下雨当且仅当地湿。
下雨 → 地湿
地湿 → 下雨
2-6. 转折/让步句按事实处理
转折/让步句不是条件句："尽管/虽然A，但B"中A、B均为事实；"就算/哪怕/即便/即使A，也B"中仅主句B为事实（A是假设，不录入）。
自然语言：尽管你不好，但是我还是对你好。
→ ～好(你)
→ 对你好(我)
自然语言：就算下雨，我也要去。
→ 去(我)
2-7. 条件+查询组合（引擎自动拆分）
用户只需说"下雨，地湿吗？"，确定性翻译器自动拆分为 规则：下雨→地湿 与 查询：?地湿——无需手动书写规则/查询结构。
自然语言：下雨，地湿吗？
下雨 → 地湿
? 地湿
SAT?
3. 否定后件推理
"后件假则前件假"是W系统的原生推理。先声明"地没湿"的事实，再查询"没下雨"。
自然语言：如果下雨地会湿，地没湿，所以没下雨。
Rain → Wet
→ ～Wet
? ～Rain
SAT?
4. 合取条件
多个前件用空格分隔，翻译为合取式。
自然语言：如果下雨且刮风，那么路滑。
Rain ∧ Wind → Slippery
5. 析取
"A或B"用 ∨ 连接。
自然语言：A或B成立。
→ A ∨ B
6. 全称量词
"所有S是P"用全称量词 ∀x(S(x) → P(x)) 表达。
自然语言：所有猫都是哺乳动物。
∀x(Cat(x) → Mammal(x))
7. 存在量词
"有些S是P"（特称命题）用存在量词 ∃x(S(x) → P(x)) 表达。存在断言需要事实支撑——由具体个体的事实声明提供主项存在性。
自然语言：有些猫是黑色的。（米米是猫且是黑色的）
∃x(Cat(x) → Black(x))
→ Cat(Mimi)
→ Black(Mimi)
SAT?
8. 关系推理
关系用谓词表示，常元用大写字母开头。
自然语言：A喜欢B。
→ Like(A, B)
9. 可废止推理
可废止推理（通则+例外）中，"例外优先"在W中通过知识库层面表达：作者在输入层给出适用的规则与事实（通常只给特例规则），引擎忠实执行。W形成规则要求蕴涵式前件为肯定原子，故例外用否定后件式表达（如 未满12岁 → ～可借书）。
自然语言：未满12岁不能借书。小红未满12岁，她能借书吗？
∀x(未满12岁(x) → ～可借书(x))
→ 未满12岁(小红)
? 可借书(小红)
SAT?
10. 查询
用 ? 标记查询目标（可多个，如 ? Wet ? Rain，引擎逐目标判定），脚本末尾用 SAT? 收尾。引擎对每个查询目标返回：结论成立、目标命题为假或未定。
自然语言：问：地湿了吗？
Rain → Wet
→ Rain
? Wet
SAT?