逆向推理

逆向推理（或逆向推理）是一种推理方法，被俗称为从目标向后工作。它被用于自动定理证明器、推理引擎、证明助手和其他人工智能应用中。逆向连锁在逻辑编程中是通过SLD解析实现的。这两种规则都是基于模因推理规则的。它是两种最常用的推理规则和逻辑含义的推理方法之一，另一种是前向连锁。

后向链从一个目标列表（或假设）开始，从结果到前因倒推，看是否有任何数据支持这些结果。一个使用后向链的推理引擎会搜索推理规则，直到找到一个与所需目标相匹配的结果（Then子句）。如果该规则的前因（If条款）已知为真，那么它就会被添加到目标列表中（要确认一个人的目标，还必须提供数据来确认这个新规则）。例如，假设一个新的宠物Fritz被放在一个不透明的盒子里，同时还有两个关于Fritz的事实。

Fritz吃苍蝇目标是根据包含以下四条规则的规则库来决定Fritz是否为绿色。因此，前项成为新的目标。弗里茨呱呱叫，弗里茨吃苍蝇3.由于这个目标是两个陈述的结合，推理引擎将其分解为两个子目标，这两个目标都必须被证明。Fritz呱呱叫Fritz吃苍蝇4.为了证明这两个子目标，推理引擎看到这两个子目标都是作为初始事实给出的。因此，连词是真的。Fritz呱呱叫和Fritz吃苍蝇因此，规则#1的前项是真的，后项也一定是真的。

弗里茨是一只青蛙因此第3条规则的前项为真，后项必为真。弗里茨是绿色的因此，这个推导允许推理引擎证明Fritz是绿色的。请注意，目标总是与含意的结果的肯定版本相匹配（而不是像模态推理那样的否定版本），即使如此，它们的前因也会被视为新的目标（而不是像肯定结果那样的结论），最终必须与已知事实（通常定义为前因总是真实的结果）相匹配；因此，使用的推理规则是模态推理。由于目标列表决定了哪些规则被选择和使用，这种方法被称为目标驱动，与数据驱动的前向连锁推理形成对比。后向链方法经常被专家系统采用。Prolog、KnowledgeMachine和ECLiPSe等编程语言在其推理引擎中支持后向链。