Prolog中的符号:-表示Implies(⇒)、Entails(⊨)还是Provable(⊢)？

先看你给出的示例代码：

mammal(dog).
mammal(cat).

animal(X) :- mammal(X).

你想明确最后一行的:-对应以下三个逻辑符号中的哪一个，同时搞懂三者的区别：

• Implies (⇒)
• Entails (⊨)
• Provable (⊢)

三个逻辑符号的核心区别 #

• Implies (⇒)：逻辑蕴涵
  这是纯逻辑层面的“如果...那么...”关系，是抽象的命题关联。比如“若X是哺乳动物，则X是动物”，它只陈述两个命题间的必然推导逻辑，和具体的证明过程、运行系统无关。
• Entails (⊨)：语义蕴涵
  指从给定的事实/公理出发，在所有可能的语义模型里，只要前提为真，结论就一定为真。简单说就是“从语义上必然成立”——比如给定mammal(dog)，所有符合这个事实的模型中，animal(dog)都一定为真，这就是语义蕴涵的体现。
• Provable (⊢)：句法可证
  这是纯过程化的概念：从系统允许的句法规则出发，通过具体的推导步骤（比如Prolog的合一、回溯搜索），能从前提推导出结论。它不关心语义是否合理，只看能不能用规则“推出来”。

Prolog中:-的准确对应 #

Prolog里的:-最直接对应的是Provable (⊢)，但我们可以从语义上把它解读为Implies(⇒)，原因如下：

1. 从运行机制看：Prolog是靠句法推导运行的——当你查询animal(X)时，它会用合一机制匹配animal(X) :- mammal(X)这条规则，然后去搜索mammal(X)是否能被证明（找到对应事实或其他规则）。整个过程完全是句法层面的证明流程，和⊢的定义完全契合。
2. 从语义解读看：我们写这条规则时，确实是想表达“如果X是哺乳动物，那么X是动物”这个逻辑蕴涵（⇒），但这只是人类赋予规则的语义，Prolog本身并不处理语义，只执行句法推导。
3. 为什么不是Entails(⊨)？语义蕴涵（⊨）是描述整个事实集合和结论之间的全局语义关系，而:-是用来构建程序中的推导规则，是推导过程的组成部分，不是用来描述这种全局关系的。

你的思考其实很到位：Prolog的符号匹配（合一与搜索）正是实现⊢的核心，而规则的语义属性是我们赋予它的⇒含义，但Prolog运行时只关注句法上的可证性。

内容的提问来源于stack exchange，提问作者Prolog ByExample