# SLD消解

> Selective Linear Definite clause resolution，Prolog等逻辑编程语言使用的推理机制，通过目标与规则的统一和回溯搜索答案。

- ID: m06855
- 分类: structure
- 领域: 逻辑学

## 定义

Selective Linear Definite clause resolution，Prolog等逻辑编程语言使用的推理机制，通过目标与规则的统一和回溯搜索答案。脚手架作用：自动化推理。将声明式知识转化为可执行的推理过程。

## 机制

在Prolog等逻辑编程语言中，SLD消解是基于"合一（unification）"与"回溯（backtracking）"的定理证明机制：从目标子句出发，用规则头部与其合一，递归求解子目标，某条路径失败则回溯到上一选择点尝试其它规则。本质是"证明某个逻辑语句是否可满足"的搜索过程。

## 练习

1) 取最左目标子句；2) 在知识库中找可与其合一的规则；3) 替换并产生新目标集；4) 递归直到目标集为空（成功）或回溯耗尽（失败）。

## 脚手架用法

自动化推理。将声明式知识转化为可执行的推理过程。

[阅读网页](https://thinkingmodels.site/entries/detail/m06855)