霍恩子句
Parent: ai_keywords
核心定义
霍恩子句（Horn Clause）是数理逻辑中的一种特殊子句，其形式为：
¬A₁ ∨ ¬A₂ ∨ … ∨ ¬Aₙ ∨ B，约束条件为包含 至多一个正文字（肯定断言）。
其中 B 是正文字（可为空），A₁…Aₙ 是负文字（否定断言）。该结构等价于蕴含式：
(A₁ ∧ A₂ ∧ … ∧ Aₙ) → B。
霍恩子句是逻辑编程（如 Prolog）的理论基石，因其在归结推理中保持封闭性，可实现高效、可回溯的自动演绎。
关键技术点
-
子句唯一性约束
每个霍恩子句最多含一个正文字。无正文字时称为“目标子句”（查询），用于推导矛盾；有正文字时则为“确定子句”（规则或事实）。 -
SLD归结机制
霍恩子句的归结仅需线性选择单条规则与目标统一，避免了一般归结的盲目组合爆炸，计算复杂度可控于多项式时间。 -
反向推理范式
Prolog 等系统以目标（肯定式）为起点，通过匹配规则头部（B），逐一将体部（A₁…Aₙ）子目标化，形成问询链。这一过程天然适合诊断类问题。 -
知识表示能力
每条规则B :- A₁, …, Aₙ.可视为 IF-THEN 逻辑片段，便于编码医学决策树、因果关系或诊断标准。 -
确定性与否定处理
霍恩子句不直接支持显式否定（封闭世界假设），但可通过“失败即否定”（Negation as Failure）实现非单调推理，适用于不完全信息的环境。
医学/神经科学应用场景
背景：首都医科大学神经病学系在帕金森病早期诊断与分级中，需要整合多模态临床证据（症状、影像、生物标记物）。
实现：采用霍恩子句构建决策支持规则库，例如：
帕金森病(患者) :- 静止性震颤(患者), 肌强直(患者), 运动迟缓(患者).
当系统需鉴别帕金森病与特发性震颤时，可进一步细化：
特发性震颤识别(患者) :- 姿势性震颤(患者), 无肌强直(患者), 无运动迟缓(患者).
系统通过 SLD 归结反向询问医生可观测症状，自动推导最可能的诊断。该框架还被用于构建药物交互预警模型：
药物禁忌(患者) :- 使用左旋多巴(患者), 使用单胺氧化酶抑制剂(患者).
霍恩子句的线性归结特性保证了推理的实时性，满足临床决策时效要求，同时规则可解释性强，便于神经科医师审阅与维护。
