Lib.rs

Chalk的核心包。

有关最新信息，请参阅Github。

lib.rs:

基于SLG算法的替代求解器，实现了良好形式的语义。有关求解器工作原理的概述，请参阅chalk书中按需SLG求解器。

此算法非常基于以下论文中找到的描述，我将在此处评论中引用为EWFS

基于良好形式的语义的有效自顶向下查询计算（Chen, Swift, and Warren; 1995年《逻辑程序设计杂志》）

然而，为了理解该论文，我建议首先从以下论文开始，我将在此处评论中引用为NFTD

带有延迟的新表格解析公式（Swift; 1999年EPIA）

此外，我还从以下论文中包含了扩展，我将分别将其称为SA和RR，它们描述了在处理子目标等时如何引入近似

具有有限三值模型的逻辑程序终止评估（Riguzzi和Swift; 2013年《计算逻辑交易》）（引入“子目标抽象”，因此命名为SA）

径向约束（Grosof和Swift; 2013年）

另一篇有用的论文是以下内容，它给出了所涉及概念的一种高层次概述，我将在此处评论中引用为XSB

XSB：将表格逻辑程序设计扩展到Prolog（Swift和Warren; 2010年《逻辑程序设计的理论与实践》）

虽然这段代码借鉴了那些论文中描述的算法，但它并不完全相同。一方面，那里的方法需要扩展到我们的上下文中，特别是应对遗传harrop谓词和我们的统一版本（产生子目标）。我认为这些扩展在很大程度上是忠实于原意的。然而，还有一些地方我故意偏离了论文中描述的语义——例如通过更积极地近似——我在这些地方加上了注释"DIVERGENCE"。这些地方可能需要在将来进行评估。

其他术语词汇表

• WAM：Warren抽象机，一种高效评估Prolog程序的方法。请参阅http://wambook.sourceforge.net/。
• HH：遗传harrop谓词。Chalk所处理的内容。由Lambda Prolog普及。