Lib.rs

The core crate for Chalk.

See Github for up-to-date information.

lib.rs:

An alternative solver based around the SLG algorithm, which implements the well-formed semantics. For an overview of how the solver works, see The On-Demand SLG Solver in the chalk book.

This algorithm is very closed based on the description found in the following paper, which I will refer to in the comments as EWFS:

Efficient Top-Down Computation of Queries Under the Well-founded Semantics (Chen, Swift, and Warren; Journal of Logic Programming '95)

However, to understand that paper, I would recommend first starting with the following paper, which I will refer to in the comments as NFTD:

A New Formulation of Tabled resolution With Delay (Swift; EPIA '99)

In addition, I incorporated extensions from the following papers, which I will refer to as SA and RR respectively, that describes how to do introduce approximation when processing subgoals and so forth:

Terminating Evaluation of Logic Programs with Finite Three-Valued Models Riguzzi and Swift; ACM Transactions on Computational Logic 2013 (Introduces "subgoal abstraction", hence the name SA)

Radial Restraint Grosof and Swift; 2013

Another useful paper that gives a kind of high-level overview of concepts at play is the following, which I will refer to as XSB:

XSB: Extending Prolog with Tabled Logic Programming (Swift and Warren; Theory and Practice of Logic Programming '10)

While this code is adapted from the algorithms described in those papers, it is not the same. For one thing, the approaches there had to be extended to our context, and in particular to coping with hereditary harrop predicates and our version of unification (which produces subgoals). I believe those to be largely faithful extensions. However, there are some other places where I intentionally diverged from the semantics as described in the papers -- e.g. by more aggressively approximating -- which I marked them with a comment DIVERGENCE. Those places may want to be evaluated in the future.

Glossary of other terms:

• WAM: Warren abstract machine, an efficient way to evaluate Prolog programs. See http://wambook.sourceforge.net/.
• HH: Hereditary harrop predicates. What Chalk deals in. Popularized by Lambda Prolog.