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