我的母体是日常蕴涵逻辑W（二值外延一阶系统）
我的推理合乎人类日常思维，可解释。
我可以嵌入需要演绎推理的场景（如LLM），提供高保真度。
为AI时代提供安全可信的逻辑基础设施。
| 维度 | W引擎 | 经典逻辑工具（HermiT等） | 经典一阶证明器（Prover9等） | 大语言模型（LLM） |
|---|---|---|---|---|
| 推理基础 | 日常蕴涵 | 实质蕴涵 | 实质蕴涵 | 统计关联 |
| 推理方式 | 日常思维（动态） | 真值函项（静态） | 真值函项（静态） | 概率生成 |
| 推理类型 | 全谱系覆盖 | 仅限于分类推理 | 仅一阶逻辑片段 | 无确定类型 |
| 推理能力 | 通过一阶饱和、三段论、关系推理、法律案例、AI幻觉纠正等16类测试 | 需语法裁剪以保证判定 | 复杂推理易崩溃 | 逻辑不可靠 |
| 查询模式 | 验证性查询（判定目标：真／假／未定）＋生成性查询（遍历根辖域原子，给出知识库完全真值快照） | 仅一致性检查 | 仅判定单个目标 | 无真值概念 |
| 可解释性 | 完整推理链，有14种推理标签和WHY追溯 | 无 | 极有限 | 事后归因（不可信） |
| 矛盾处理 | 精确定位不扩散 | 报告不一致 | 推导空子句 | 输出混乱 |
| 三值判定 | 一次推理，根辖域自然分流为真/假/未定，无需二次归谬 | 仅二值，需二次推理区分"未定" | 仅可证/不可证 | 无真值概念，概率猜测 |
| 可判定性保证 | 双层防线。理论层：从源头规避不可判定性根源，基于W-ALC子模型的FMP保证。工程层：惰性实例化、分层唤醒、等价类剪枝等减负设计，辅以步数/常元/深度三重硬限制。 | 语法裁剪 | 无保证 | 无保证 |
| 工程完成度 | 推理内核已完成鲁棒性验证。外围配套（API、CoT验证器、翻译指南、结构分析器）已就绪。 | 十余年发展，相对成熟 | 十余年发展，相对成熟 | 快速迭代中 |
💡 以上能力均可通过下方「自定义推理」区域进行验证。输入W脚本，点击运行，引擎将实时返回判定及完整推理链。
以下案例展示W引擎无效蕴涵阻塞、否定后件原生支持、矛盾精确定位不扩散、多条件排除锁定、三值判定等特性。
场景：教务处通知"所有学生都必须参加期末考试"，后又补充"因病住院的学生可以不参加"。小明因病住院，小红正常上课。小明需要参加考试吗？小红呢？
经典逻辑：既然小明被要求"必须参加"，又"可以不参加"，这不矛盾吗？从矛盾中可以得出任何结论，小红小明参加不参加都可以。（矛盾推出一切，整个系统崩溃。）
LLM：麻烦了，有矛盾！我想想是回避问题呢还是给出模棱两可的回答呢？（有时LLM也会编个似是而非的回答，企图自圆其说。）
W引擎：小明因病住院，触发"可以不参加考试"为真；同时小明是学生，触发"必须参加考试"为真。等价类前置检测发现冲突，矛盾被精确定位在"参加考试(小明)"——它被同时要求为真和假。知识库整体判定为不一致（UNSAT），但引擎不爆炸：它不会像经典逻辑那样从矛盾推出任意结论。小红的推理通道未被污染——事实"学生(小红)"保持为真不被撤销；在不含矛盾的知识库中，小红可正常推出"必须参加考试"（见下）。这里"学生须参加"是通则、"住院可不参加"是例外，两者后件冲突被引擎检出——这正是可废止冲突的检测（例外优先的最终裁决见AI案例7说明）。想知道小明参加不参加？请看AI案例7——可废止推理。
查询：参加考试(小红)?（知识库不含小明的矛盾事实时）
结论：✅ 结论成立（小红必须参加考试）——矛盾被隔离，小红的通道完好
▶ 查看引擎推理链特性：矛盾被精准定位在局部，不爆炸、不扩散。含矛盾时引擎报告整体UNSAT但精确定位矛盾原子；已赋值的无关事实（学生(小红)）不被撤销；不含矛盾时小红的推理通道照常推出结论。
场景：商场规定"会员购物可享九折优惠"。老王不是会员，老李是会员。老王能享受九折吗？老李呢？
经典逻辑：虽然老王不是会员，前件假，蕴涵式就真。但这能推出老王享受九折吗？能。那能推出老王不享受九折吗？也能啊。（实质蕴涵无法区分"规则本身成立"和"规则在当前情况下适用"。）
LLM：老王不是会员，那肯定没有九折吧？但也许商场有促销活动呢？或者会员规则有例外？（LLM可能给出模棱两可的回答，无法严格区分"规则不适用"和"规则被违反"。）
W引擎：老王不是会员，前件为假，直接阻塞蕴涵式，我保持沉默。老李是会员，前件为真，蕴涵式正常激活，推出老李享受九折。
查询：九折(老王)? 九折(老李)?
结论：⚠️ 老王未定（前提不足）；✅ 老李可以（享受九折）
▶ 查看引擎推理链特性：该沉默时沉默，该说话时说话，不猜、不编，严守"逻辑纪律"——规则不适用时绝不强行推理，规则适用时严格遵守推理规则。
场景：公司规定"迟到会被扣全勤奖"。月底小张的全勤奖正常发放。他迟到过吗？
经典逻辑：假设小张迟到，推出全勤奖被扣，与事实矛盾，故小张没迟到。（经典逻辑需要绕道反证法找答案。）
LLM：全勤奖没扣，那可能没迟到吧？但也可能迟到了但主管忘了记录？或者迟到被豁免了？（LLM犹豫不决，无法给出确定性结论。）
W引擎：后件为假，触发反向传播，一步推出"迟到"为假。
查询：迟到?
结论：❌ 结论为假（小张没迟到）
▶ 查看引擎推理链特性：原生支持否定后件推理——后件假→前件必假，O(1)到位。
场景：某小区发生入室盗窃案，警方锁定嫌疑人只能是张三、李四、王五、赵六。经查案发时，张三正在外地出差（有高铁记录），李四在单位加班（有监控证明），王五在医院住院（有病历证明）。三人均无作案可能。问：可否推定赵六是作案人？
经典逻辑：排除了张三、李四、王五，那剩下赵六？不行，我无法从后件真去推前件真假啊！
LLM：大概率是赵六干的吧？但万一是其他人干的呢？（LLM可能基于统计常识"合理猜测"。）
W引擎：四条通道汇聚于"作案发生"。张三通道被排除，李四通道被排除，王五通道被排除——唯一剩余通道是赵六。后件"作案发生"为真，前件"赵六作案"必为真。
查询：作案(赵六)?
结论：✅ 结论成立（赵六是作案人）
▶ 查看引擎推理链特性：多通道条件下，通过排除其他前件，唯一通道被还原为单通道，在演算中完成纯真值化，从不确定中涌现确定性。不是概率猜测，是逻辑必然。
场景：如果感染流感，则会发烧。如果感染新冠，也会发烧。患者发烧了。问：患者感染流感了吗？
经典逻辑：我得做两次推理——先判SAT，再假设"没感染流感"做归谬验证。（经典SAT求解器需要二次归谬验证才能区分"假"和"不确定"。）
LLM：发烧了应该是流感吧？但也可能是其他原因……我不确定。（LLM的"不确定"是概率性的，没有严格的逻辑依据。）
W引擎：这是多通道条件，后件发烧为真，但流感不是唯一前件，引擎的回答只能是"未定"。
查询：流感?
结论：⚠️ 未定（前提不足）
▶ 查看引擎推理链特性：推理结束，真、假、未定三种结果一次分流，全在根辖域中，谁真、谁假、谁未定，一清二楚。
以下案例展示LLM在演绎推理中的典型错误及W引擎的校正，末尾案例展示W引擎对可废止推理这一日常推理形态的支持（当前实现到冲突检测）。
场景：规定"作弊→成绩取消"（知识库声明两条通道：作弊→成绩取消、系统误判→成绩取消）。小明的成绩被取消了，他作弊了吗？
LLM：成绩被取消了，那肯定是作弊了吧。（LLM常犯肯定后件谬误：从后件真反推前件真，却忽略了其他可能的通道。）
W引擎：后件"成绩取消"为真，但知识库声明了两条通道：作弊→成绩取消、系统误判→成绩取消，两条都未排除。多通道（充分条件）条件下，后件真无法锁定任何单一前件，我保持沉默。
结论：⚠️ 未定
▶ 查看引擎推理链可运行脚本（复制到下方自定义推理区即可）：
点睛：LLM从结果反推原因，引擎严守逻辑纪律。
场景：因为接种疫苗，所以产生抗体（知识库声明两条通道：接种疫苗→产生抗体、自然感染→产生抗体）。检测产生了抗体，接种疫苗了吗？
LLM：产生抗体了，那肯定接种过疫苗。（LLM常会混淆因果关系，忽略其他可能的原因通道。）
W引擎：这跟案例1是一家人——后件"产生抗体"为真，但知识库声明了两条通道：接种疫苗→产生抗体、自然感染→产生抗体，都未排除，无法锁定，我当然继续保持沉默。
结论：⚠️ 未定
▶ 查看引擎推理链可运行脚本（复制到下方自定义推理区即可）：
点睛：LLM颠倒因果，引擎坚持"多通道条件下后件真不能锁定单一前件"。案例1和案例2虽然场景不同——一个是规则性充分条件，一个是因果性充分条件——但在逻辑上同属肯定后件谬误。
场景：假如猫是爬行动物，那么猫会下蛋。现在告诉你：猫确实是爬行动物。问：猫会下蛋吗？
LLM：猫怎么会是爬行动物？这个假设不成立！但如果是真的，那猫会下蛋？（LLM常在虚拟前提与现实常识间纠结，要么拒绝推理，要么陷入认知冲突。）
W引擎：我不关心前提的真假，只负责推理的有效性。既然前件"猫是爬行动物"被设为真，那么后件"猫会下蛋"必然为真。
结论：✅ 结论成立（猫会下蛋）
▶ 查看引擎推理链点睛：引擎只管推理形式有效，不管前提内容真假。案例1、2、3分别是三种条件句——普通充分条件、因果条件、反事实虚拟条件——但引擎均可统一处理，因为其语义基座日常蕴涵能统一刻画这三种条件句。
场景：审批需"预算超100万且需外部合作"。预算120万，无外部合作。需要审批吗？
LLM：预算够了，那就审批吧。（LLM容易只看主要条件，遗漏次要前提。）
W引擎：外部合作为假，合取未满足，前件为假，这比案例1复杂一点点，但还是一家人，我保持沉默。
结论：⚠️ 未定
▶ 查看引擎推理链点睛：LLM遗漏前提，引擎要求前提"缺一不可"，确认全部为真后，才会启动推理。
场景：闹钟响小明就起床。小明没起床。
LLM：闹钟可能没响，也可能响了小明没听见。（LLM犹豫不决，无法给出确定性结论。）
W引擎：后件假，反向传播直接推出前件假。
结论：❌ 结论为假（闹钟没响）
▶ 查看引擎推理链点睛：LLM犹豫不决，引擎O(1)一步到位。
场景：研究发现，长期吸烟的人群肺癌发病率更高（知识库声明两条通道：长期吸烟→肺癌、遗传易感→肺癌）。小王得了肺癌，他一定长期吸烟吗？
LLM：得肺癌的人大部分都吸烟，那小王应该也是长期吸烟者。（LLM常将统计相关性误判为逻辑必然性，忽略其他可能通道。）
W引擎：统计相关不等于逻辑蕴涵。后件"肺癌"为真，但知识库声明了两条通道：长期吸烟→肺癌、遗传易感→肺癌，都未排除，多通道条件下无法锁定，我的回答是"未定"。
结论：⚠️ 未定
▶ 查看引擎推理链可运行脚本（复制到下方自定义推理区即可）：
点睛：统计概率不能代替逻辑推导。引擎严守推理纪律，不把"很可能"当成"必然"。
场景：鸟类都会飞（通则），企鹅是例外（不会飞）。Tweety 是企鹅，麻雀是鸟。Tweety 会飞吗？
LLM：按"鸟会飞"的统计关联直接答"会飞"，忽略企鹅例外；或面对通则与例外同时存在时含糊其辞、两头摇摆。
W引擎：知识库声明优先级 企鹅→～会飞 > 鸟→会飞（例外优先）——优先关系由知识层显式设定，可废止外挂执行"例外优先"的裁决：例外规则对 Tweety 胜出，推出 Tweety 不会飞；麻雀作为普通个体，通则照常作用于它，推出麻雀会飞。裁决具体到个例，互不影响。
结论：❌ Tweety 不会飞（例外优先裁决）；麻雀照常会飞（✅）
▶ 查看引擎推理链（裁决子任务）麻雀对照：查询 ? 会飞(麻雀) → ✅ 结论成立（通则照常作用于非例外个体，例外裁决不波及）。
可运行脚本（复制到下方"自定义推理"即可）：
点睛：可废止推理 = 通则 + 例外 + 优先级声明（例外优先）。优先关系是知识层的显式设定，逻辑只负责执行"例外优先"的推演（书稿第十二章"设定的完整性"）；裁决具体到个例——Tweety 不会飞、麻雀照常会飞、通则本身不变。例外裁决由独立外挂模块完成，引擎核心零改动。
法律推理是形式逻辑最严格的应用场景之一。以下六个案例展示法律逻辑中最核心的六种推理类型在W引擎中的（一阶谓词）形式化验证。
场景：甲为精神病人，监护人未同意，甲与乙签订房屋买卖合同。该合同无效吗？
法律依据：《民法典》第144条：无民事行为能力人实施的民事法律行为无效。
结论：✅ 结论成立（合同无效）
▶ 查看引擎推理链（推理链中FORALL_INST多次出现，是引擎对嵌套量词∀x∀y进行全称实例化的正常行为，不影响推理结果。）
场景：甲偷乙手机卖给不知情的丙。丙能取得所有权吗？
法律依据：《民法典》第311条：赃物不适用善意取得。
结论：❌ 结论为假（丙不能取得所有权）
▶ 查看引擎推理链场景：甲持盖有乙公司公章的空白合同与丙签约，乙未授权但公章真实。代理行为有效吗？
法律依据：《民法典》第172条：相对人有理由相信行为人有代理权的，代理行为有效。
结论：✅ 结论成立（代理行为有效）
▶ 查看引擎推理链场景：丈夫借款用于赌博，妻子不知情且未受益。属于夫妻共同债务吗？
法律依据：《民法典》第1064条：超出家庭日常生活需要的债务，不属于夫妻共同债务。
结论：❌ 结论为假（不属于夫妻共同债务）
▶ 查看引擎推理链场景：小区10楼抛物砸伤人，未定具体住户。住户A能自证清白，不用承担责任。住户B是否要承担补偿责任？
法律依据：《民法典》第1254条：难以确定具体侵权人的，除能证明自己不是侵权人的外，由可能加害的建筑物使用人给予补偿。
结论：⚠️ 未定（住户B是否承担补偿责任，取决于能否证明自己不是侵权人——这恰恰体现了立法目的：无法自证清白者才需承担补偿责任。住户A能自证清白被排除，住户B的自证清白状态未给定，故未定。）
▶ 查看引擎推理链场景：公司章程规定"股东查阅账簿需董事会批准"，与《公司法》第33条冲突。股东能直接查阅吗？
法律依据：《公司法》第33条：股东有权查阅公司账簿，公司章程不得实质性剥夺。
结论：❌ 结论为假（引擎严格执行章程规则，股东无权直接查阅。这并非引擎的推理缺陷——引擎是"空壳"，只忠实地执行给定的规则，不预设任何法价值判断。现实中法院会依据上位法优先原则支持股东查阅权，而引擎的价值正在于：它诚实地告诉你"给定这些规则，推出了什么结论"。如果结论不符合上位法，说明规则本身需要修正——这正是逻辑系统在法律领域作为"规则审查工具"的关键作用。）
▶ 查看引擎推理链选择以下任一经典逻辑谜题，点击选项按钮，引擎将实时返回推理结果与完整推理链。
同一套推演内核、同一张约束图、同一组原子值，两种查询模式：验证性查询判定某个目标命题；生成性查询遍历根辖域全部原子，输出知识库的完全真值快照。
💡 语法：蕴涵式 A → B | 事实 → A 或 → ～A | 问结论 ? 目标（如 ? Wet）| 全称 ∀x(P(x)→Q(x)) | 高级：SAT?（判定知识库可满足性）
📖 查看推理类型谱系 | 查看翻译指南
🐛 发现Bug或有功能建议？欢迎反馈至页面底部邮箱。
W引擎以日常蕴涵替代经典逻辑的实质蕴涵作为语义底座，以"同真同假"为真值条件，带来了否定后件式恢复原生地位、蕴涵链自动形成等价类、矛盾不再爆炸、三值判定一次分流四个根本性改变。W系统具备一致性、完全性、可判定性三项元逻辑证明。485项全量测试全部通过。提供Python API和HTTP服务接口。 查看完整白皮书 →
覆盖日常演绎推理类型，含迄今能汇总的全部类型（九大类）：基本逻辑规律、三段论与直言推理、假言推理、选言与联言推理、充要条件推理、关系推理、命题逻辑基本推理、间接证明、经典逻辑未覆盖的日常推理模式。 查看完整谱系 →
覆盖单元测试、特性测试、定理测试、解析器测试、一阶测试、一阶饱和测试、三段论24式严格测试、关系推理测试、命题补充测试、AI幻觉纠正测试、端到端LLM集成测试、法律案例测试、知识库管理测试、确定性翻译测试、可废止推理测试、生成性查询测试共16类；另有五道合法性检验（详见测试套件页）。 查看完整测试数据 →
API端点：POST https://w-engine.top/query/sat
请求体为W脚本文本，返回JSON（结论成立/结论为假/未定、推理链、摘要）。
curl -X POST https://w-engine.top/query/sat -d 'Rain → Wet → Rain ? Wet SAT?'
| 推理标签 | 含义 |
|---|---|
| FACT | 事实声明 |
| FORWARD | 前向传播（肯定前件式） |
| BACKWARD | 反向传播（否定后件式） |
| EQUIV_SYNC | 等价同步 |
| CONFLICT | 冲突检测 |
| BLOCK | 阻塞（无效蕴涵排除） |
| ASSUME | 假设（进入辖域） |
| CONCLUSION | 结论（退出辖域） |
| BACKTRACK | 回溯作废 |
| OR_BRANCH | 析取分支 |
| FORALL_INST | 全称实例化 |
| EXISTS_INST | 存在实例化 |
| EXIST_COMMIT | 存在承诺 |
| EQUIV_MERGE | 等价合并 |
因申报课题需要匿名，研究者个人信息及联系方式等暂时屏蔽，不便之处，见谅。