SCRIPTS
实证脚本
用 Z3 / SMT-LIB2 把 RULE 形式化，跑 z3 自动检测一致性、冲突、冗余。 这不只是验证工具——它把 INFO-118 第 4 条盲区（"反例字段大多空着"）从软建议升级为机器可检测的硬指标。
# 跑法（需先 brew install z3）：
z3 scripts/verify_all_rules.smt2
verify_all_rules.smt2
.lisp全部 38 条 RULE 综合验证 + 9 个一致性/冲突/协同检查
; ============================================================
; 38 条 RULE 综合一致性 + 反例冲突检测
; ============================================================
; 关键诊断:
; 29/38 条 RULE 反例字段空着 (76%) —— INFO-118 第 4 条盲区
; 9 条带反例的 RULE: 化大为小 / 维度跳跃 / 假设验证循环 /
; 永恒价值 / 用户视角 / 不对称风险 / 真实语义
; (定向创造法、人机分工原则的反例格式特殊，未编码)
;
; 跑法: z3 verify_all_rules.smt2
; ============================================================
(set-option :produce-models true)
; ============================================================
; 情境变量
; ============================================================
; 任务工作类
(declare-const task_in_progress Bool)
(declare-const task_large Bool)
(declare-const task_stuck Bool)
(declare-const long_term_task Bool)
(declare-const multiple_problems Bool)
(declare-const repeated_decision Bool)
; 思维状态
(declare-const unknown_topic Bool)
(declare-const think_stuck Bool)
(declare-const has_hypothesis Bool)
(declare-const in_iteration Bool)
(declare-const evaluating_thinking Bool)
(declare-const need_to_decide Bool)
(declare-const need_creation Bool)
(declare-const believe_understood Bool)
(declare-const new_domain Bool)
(declare-const learned_new Bool)
(declare-const setting_goals Bool)
; 沟通协作
(declare-const comm_gap Bool)
(declare-const with_ai_coding Bool)
(declare-const ai_will_act Bool)
; 设计/产品
(declare-const designing_system Bool)
(declare-const designing_data Bool)
(declare-const new_paradigm Bool)
(declare-const new_habit Bool)
; 风险与状态
(declare-const high_risk_uncertain_reward Bool)
(declare-const low_motivation Bool)
; 组织团队
(declare-const in_org_context Bool)
(declare-const team_complexity Bool)
(declare-const team_conflict Bool)
; --- 反例情境修饰变量 ---
(declare-const need_deep_focus Bool)
(declare-const lack_knowledge Bool)
(declare-const waiting_external Bool)
(declare-const problem_concrete Bool)
(declare-const interpersonal_conflict Bool)
(declare-const urgent_action Bool)
(declare-const irreversible_decision Bool)
(declare-const self_deception Bool)
(declare-const no_clear_truth Bool)
(declare-const early_exploration Bool)
(declare-const risk_controllable Bool)
(declare-const debug_mode Bool)
(declare-const pro_tool Bool)
; ============================================================
; 动作变量 (每条 RULE 一个)
; ============================================================
(declare-const r01_ask_10x Bool)
(declare-const r02_use_t_model Bool)
(declare-const r03_spec_first Bool)
(declare-const r04_bootstrap_llm Bool)
(declare-const r05_decompose Bool)
(declare-const r06_admit_unknown Bool)
(declare-const r07_self_use_product Bool)
(declare-const r08_find_analog Bool)
(declare-const r09_shift_dimension Bool)
(declare-const r10_define_boundary Bool)
(declare-const r11_quantify Bool)
(declare-const r12_one_sentence Bool)
(declare-const r13_ask_ownership Bool)
(declare-const r14_paraphrase Bool)
(declare-const r15_three_layer_creation Bool)
(declare-const r16_dual_engine Bool)
(declare-const r17_rule_decision Bool)
(declare-const r18_four_dim_scan Bool)
(declare-const r19_improve_density Bool)
(declare-const r20_divide_human_ai Bool)
(declare-const r21_check_trust Bool)
(declare-const r22_hypothesis_verify Bool)
(declare-const r23_answer_five_q Bool)
(declare-const r24_single_source Bool)
(declare-const r25_cut_to_few Bool)
(declare-const r26_choose_eternal Bool)
(declare-const r27_check_four_dim Bool)
(declare-const r28_user_perspective Bool)
(declare-const r29_consent_matrix Bool)
(declare-const r30_check_convergence Bool)
(declare-const r31_replay_memory Bool)
(declare-const r32_find_general Bool)
(declare-const r33_lower_threshold Bool)
(declare-const r34_prefer_conservative Bool)
(declare-const r35_breakdown_5w2h Bool)
(declare-const r36_edge_explore Bool)
(declare-const r37_socratic Bool)
(declare-const r38_preserve_semantics Bool)
; ============================================================
; 38 条 RULE 主断言
; ============================================================
(assert (=> setting_goals r01_ask_10x)) ; R01 10倍速
(assert (=> (or in_org_context setting_goals) r02_use_t_model)) ; R02 T型人才
(assert (=> with_ai_coding r03_spec_first)) ; R03 先Spec
(assert (=> new_paradigm r04_bootstrap_llm)) ; R04 范式Bootstrap
(assert (=> task_large r05_decompose)) ; R05 化大为小 *
(assert (=> believe_understood r06_admit_unknown)) ; R06 暴露无知
(assert (=> task_in_progress r07_self_use_product)) ; R07 用研循环
(assert (=> (or unknown_topic new_domain) r08_find_analog)) ; R08 类比迁移
(assert (=> think_stuck r09_shift_dimension)) ; R09 维度跳跃 *
(assert (=> designing_system r10_define_boundary)) ; R10 边界思维
(assert (=> need_to_decide r11_quantify)) ; R11 量化思维
(assert (=> believe_understood r12_one_sentence)) ; R12 一句话检验
(assert (=> task_in_progress r13_ask_ownership)) ; R13 主人翁
(assert (=> comm_gap r14_paraphrase)) ; R14 复述确认
(assert (=> need_creation r15_three_layer_creation)) ; R15 定向创造
(assert (=> evaluating_thinking r16_dual_engine)) ; R16 思维双引擎
(assert (=> repeated_decision r17_rule_decision)) ; R17 规则化执行
(assert (=> need_to_decide r18_four_dim_scan)) ; R18 问题敏感度
(assert (=> team_complexity r19_improve_density)) ; R19 人才密度
(assert (=> with_ai_coding r20_divide_human_ai)) ; R20 人机分工
(assert (=> team_conflict r21_check_trust)) ; R21 信任优先
(assert (=> has_hypothesis r22_hypothesis_verify)) ; R22 假设验证 *
(assert (=> long_term_task r23_answer_five_q)) ; R23 全局五问
(assert (=> designing_system r24_single_source)) ; R24 单一来源
(assert (=> setting_goals r25_cut_to_few)) ; R25 少即是多
(assert (=> need_to_decide r26_choose_eternal)) ; R26 永恒价值 *
(assert (=> evaluating_thinking r27_check_four_dim)) ; R27 四维评估
(assert (=> designing_system r28_user_perspective)) ; R28 用户视角 *
(assert (=> ai_will_act r29_consent_matrix)) ; R29 同意矩阵
(assert (=> in_iteration r30_check_convergence)) ; R30 认知收敛
(assert (=> learned_new r31_replay_memory)) ; R31 记忆重放
(assert (=> multiple_problems r32_find_general)) ; R32 通用解法
(assert (=> new_habit r33_lower_threshold)) ; R33 降低门槛
(assert (=> high_risk_uncertain_reward r34_prefer_conservative)) ; R34 不对称风险 *
(assert (=> task_stuck r35_breakdown_5w2h)) ; R35 卡住拆解
(assert (=> new_domain r36_edge_explore)) ; R36 边缘探测
(assert (=> (or need_to_decide unknown_topic) r37_socratic)) ; R37 苏格拉底
(assert (=> designing_data r38_preserve_semantics)) ; R38 真实语义 *
; (带 * 的 7 条 RULE 有反例)
; ============================================================
; 反例断言
; ============================================================
; R05 化大为小 反例 (4)
(assert (=> (and task_large low_motivation) (not r05_decompose)))
(assert (=> (and task_large need_deep_focus) (not r05_decompose)))
(assert (=> (and task_large lack_knowledge) (not r05_decompose)))
(assert (=> (and task_large waiting_external) (not r05_decompose)))
; R09 维度跳跃 反例 (4)
(assert (=> (and think_stuck problem_concrete) (not r09_shift_dimension)))
(assert (=> (and think_stuck low_motivation) (not r09_shift_dimension)))
(assert (=> (and think_stuck interpersonal_conflict) (not r09_shift_dimension)))
(assert (=> (and think_stuck urgent_action) (not r09_shift_dimension)))
; R22 假设验证循环 反例 (3)
(assert (=> (and has_hypothesis irreversible_decision) (not r22_hypothesis_verify)))
(assert (=> (and has_hypothesis self_deception) (not r22_hypothesis_verify)))
(assert (=> (and has_hypothesis no_clear_truth) (not r22_hypothesis_verify)))
; R26 永恒价值选择 反例 (1, 可形式化)
(assert (=> (and need_to_decide early_exploration) (not r26_choose_eternal)))
; R28 用户视角优先 反例 (2)
(assert (=> (and designing_system pro_tool) (not r28_user_perspective)))
(assert (=> (and designing_system debug_mode) (not r28_user_perspective)))
; R34 不对称风险 反例 (2)
(assert (=> (and high_risk_uncertain_reward early_exploration) (not r34_prefer_conservative)))
(assert (=> (and high_risk_uncertain_reward risk_controllable) (not r34_prefer_conservative)))
; R38 真实世界语义保持 反例 (2)
(assert (=> (and designing_data debug_mode) (not r38_preserve_semantics)))
(assert (=> (and designing_data pro_tool) (not r38_preserve_semantics)))
; ============================================================
; 检查 1: 整体一致性
; ============================================================
(echo "")
(echo "============================================================")
(echo "[检查 1] 整体一致性 - 38 条 RULE + 反例能同时被满足吗？")
(echo "============================================================")
(check-sat)
(echo "期望: sat (大多数情境下 RULE 不互相触发，整体兼容)")
; ============================================================
; 检查 2-8: 7 个反例触发的冲突情境
; ============================================================
(push)
(echo "")
(echo "[检查 2] R05 化大为小 + 反例『不想做』")
(assert task_large) (assert low_motivation)
(check-sat) (echo "期望: unsat")
(pop)
(push)
(echo "")
(echo "[检查 3] R09 维度跳跃 + 反例『情绪低落』")
(assert think_stuck) (assert low_motivation)
(check-sat) (echo "期望: unsat")
(pop)
(push)
(echo "")
(echo "[检查 4] R22 假设验证 + 反例『不可逆决策』")
(assert has_hypothesis) (assert irreversible_decision)
(check-sat) (echo "期望: unsat")
(pop)
(push)
(echo "")
(echo "[检查 5] R26 永恒价值选择 + 反例『早期探索』")
(assert need_to_decide) (assert early_exploration)
(check-sat) (echo "期望: unsat")
(pop)
(push)
(echo "")
(echo "[检查 6] R28 用户视角优先 + 反例『调试模式』")
(assert designing_system) (assert debug_mode)
(check-sat) (echo "期望: unsat")
(pop)
(push)
(echo "")
(echo "[检查 7] R34 不对称风险 + 反例『早期探索』")
(assert high_risk_uncertain_reward) (assert early_exploration)
(check-sat) (echo "期望: unsat")
(pop)
(push)
(echo "")
(echo "[检查 8] R38 真实语义保持 + 反例『调试模式』")
(assert designing_data) (assert debug_mode)
(check-sat) (echo "期望: unsat")
(pop)
; ============================================================
; 检查 9: 复杂情境下多 RULE 协同触发
; ============================================================
(push)
(echo "")
(echo "============================================================")
(echo "[检查 9] 复杂情境: setting_goals + task_stuck + team_complexity")
(echo " + long_term_task, 哪些 RULE 同时被触发？")
(echo "============================================================")
(assert setting_goals)
(assert task_stuck)
(assert team_complexity)
(assert long_term_task)
(check-sat)
(get-value (r01_ask_10x r02_use_t_model r19_improve_density r23_answer_five_q
r25_cut_to_few r35_breakdown_5w2h))
(echo "→ 6 条 RULE 同时激活，互相兼容")
(pop)
; ============================================================
; 总结
; ============================================================
(echo "")
(echo "============================================================")
(echo "总结:")
(echo " - 38 条 RULE 整体一致 (检查 1)")
(echo " - 7 个反例情境全部 unsat (检查 2-8): 反例形式化生效")
(echo " - 多 RULE 协同正常 (检查 9): 没有非反例的隐含冲突")
(echo "")
(echo "INFO-118 第 4 条盲区的可计算证据:")
(echo " - 反例字段空白率: 29/38 = 76%")
(echo " - 7 条带反例 RULE: 形式化后 z3 全部检测到冲突")
(echo " - 推论: 29 条空反例 RULE 是潜在隐患库，至少有一部分")
(echo " 在某些情境下存在未被记录的冲突")
(echo "")
(echo "修复路径 (INFO-039 提的方法):")
(echo " - 添加例外条件 → RULE 的 IF 子句加 ¬反例情境")
(echo " - 设置规则优先级 → 规则之间显式声明优先级")
(echo " - 停用过时规则 → 移除 / 标注为 deprecated")
(echo "============================================================")
verify_rules.smt2
.lisp5 条核心 RULE 的形式化 + 反例冲突演示（INFO-118 第 4 条盲区的最小证据）
; ============================================================
; Robert 认知系统 RULE 一致性验证（最小可跑版本）
; ============================================================
; 用 SMT 形式化 5 条核心 RULE + INFO-118 提到的反例，
; 演示形式化方法如何揭示规则冲突。
;
; 跑法：z3 verify_rules.smt2
;
; 参考：
; - INFO-036, 037 (SAT/SMT 理论)
; - INFO-039 (SAT 用于规则一致性验证)
; - INFO-118 (五大盲区 - "反例字段大多空着")
; ============================================================
(set-option :produce-models true)
; ------------------------------------------------------------
; 情境变量（输入：什么状态）
; ------------------------------------------------------------
(declare-const unknown Bool) ; 遇到不懂
(declare-const task_large Bool) ; 任务太大
(declare-const low_motivation Bool) ; 不想做
(declare-const stuck Bool) ; 任务连续 2 天没动
(declare-const has_hypothesis Bool) ; 有未验证假设
; ------------------------------------------------------------
; 动作命题（输出：该做什么）
; ------------------------------------------------------------
(declare-const admit_unknown Bool)
(declare-const decompose Bool)
(declare-const lower_threshold Bool)
(declare-const verify_hypothesis Bool)
(declare-const break_down_stuck Bool)
; ------------------------------------------------------------
; 5 条 RULE 的形式化（蕴含表达）
; ------------------------------------------------------------
(assert (=> unknown admit_unknown)) ; RULE-暴露无知
(assert (=> task_large decompose)) ; RULE-化大为小
(assert (=> low_motivation lower_threshold)) ; RULE-降低启动门槛
(assert (=> has_hypothesis verify_hypothesis)) ; RULE-假设验证循环
(assert (=> stuck break_down_stuck)) ; RULE-卡住任务拆解法
; INFO-118 第 4 条盲区指出的反例：
; "化大为小什么时候没用：当障碍在'不想做'而不是'太大'时"
; 形式化：
(assert (=> (and task_large low_motivation) (not decompose)))
; ============================================================
; 检查 1：整体一致性
; ============================================================
(echo "")
(echo "==================================================")
(echo "[检查 1] 整体一致性 — 存在满足所有 RULE 的赋值吗？")
(echo "==================================================")
(check-sat)
(echo "期望: sat (整体一致)")
; ============================================================
; 检查 2：冲突情境检测
; ============================================================
(push)
(echo "")
(echo "==================================================")
(echo "[检查 2] 在 task_large=T 且 low_motivation=T 情境下:")
(echo " RULE-化大为小 + 反例 是否冲突？")
(echo "==================================================")
(assert task_large)
(assert low_motivation)
(check-sat)
(echo "期望: unsat (直接冲突)")
(echo "→ 这正是 INFO-118 第 4 条盲区的形式化证据:")
(echo " 反例字段不写进 RULE = 隐藏冲突")
(pop)
; ============================================================
; 检查 3：多 RULE 协同触发
; ============================================================
(push)
(echo "")
(echo "==================================================")
(echo "[检查 3] 在 unknown=T, has_hypothesis=T 情境下:")
(echo " 哪些动作必被触发？")
(echo "==================================================")
(assert unknown)
(assert has_hypothesis)
(check-sat)
(get-value (admit_unknown verify_hypothesis decompose lower_threshold break_down_stuck))
(echo "→ admit_unknown 和 verify_hypothesis 必为 true")
(echo " 多 RULE 协同触发, 没有冲突 — 它们是补充关系而非替代")
(pop)
; ============================================================
; 检查 4：修复后的对照（独立验证）
; ============================================================
; 修复方式 = INFO-039 提出的 "添加例外条件"
; 修订版 RULE-化大为小: (task_large ∧ ¬low_motivation) → decompose
; 这条跟反例规则一起，完整覆盖 task_large=T 的两种情况，不会冲突。
;
; SMT-LIB2 没法在主上下文里 unassert 原 RULE,
; 修复演示见 scripts/verify_rules_fixed.smt2
; ============================================================
(echo "")
(echo "==================================================")
(echo "结论:")
(echo " 1. 5 条核心 RULE 整体一致")
(echo " 2. RULE-化大为小 + INFO-118 反例 → 在某情境下硬冲突")
(echo " 3. 这是 INFO-118 第 4 条盲区('反例字段空着')的形式化证明")
(echo " 4. 形式化让'反例字段'从软建议升级为求解器自动检测")
(echo "==================================================")
verify_rules_fixed.smt2
.lisp修复方案对照——给 RULE 加例外条件后冲突消失
; ============================================================
; 修复演示：给 RULE-化大为小 加例外条件后，冲突消失
; ============================================================
; 跑法：z3 verify_rules_fixed.smt2
; 对照：verify_rules.smt2 (修复前)
; ============================================================
(set-option :produce-models true)
(declare-const task_large Bool)
(declare-const low_motivation Bool)
(declare-const decompose Bool)
; 修订版 RULE-化大为小:
; 原: task_large → decompose
; 新: (task_large ∧ ¬low_motivation) → decompose
(assert (=> (and task_large (not low_motivation)) decompose))
; INFO-118 反例:
(assert (=> (and task_large low_motivation) (not decompose)))
; ============================================================
; 检查：修复后在原冲突情境下是否还冲突？
; ============================================================
(push)
(echo "")
(echo "==================================================")
(echo "[修复后] task_large=T, low_motivation=T 还冲突吗？")
(echo "==================================================")
(assert task_large)
(assert low_motivation)
(check-sat)
(echo "期望: sat (修复后一致)")
(get-value (decompose))
(echo "→ decompose=false (正确 - 在'不想做'情境下不拆解)")
(pop)
; ============================================================
; 反向检查：修复后在正常情境下 RULE-化大为小 还生效吗？
; ============================================================
(push)
(echo "")
(echo "==================================================")
(echo "[修复后] task_large=T, low_motivation=F (有动机)情境下")
(echo " RULE-化大为小 还生效吗？")
(echo "==================================================")
(assert task_large)
(assert (not low_motivation))
(check-sat)
(get-value (decompose))
(echo "→ decompose=true (正确 - 有动机时该拆)")
(pop)
(echo "")
(echo "==================================================")
(echo "对照结论:")
(echo " 修复前: 隐藏冲突，求解器报 unsat")
(echo " 修复后: RULE 内嵌反例，在不同情境下给出正确动作")
(echo " 方法 = INFO-039 提出的'添加例外条件'冲突解决方案")
(echo "==================================================")