Tabled Resolution

Besides SLD resolution SOUL also features SLG resolution, also known as tabled resolution. The following program will illustrate the advantages of SLG resolution:

Besides SLD resolution SOUL also features SLG resolution, also known as tabled resolution. The following program will illustrate the advantages of SLG resolution:
tabled ?from path: ?to if
  ?from path: ?somewhere,
  ?somewhere edge: ?to
tabled ?from path: ?to if
  ?from edge: ?to
This is a simple way to define a path in a graph between two nodes. Two nodes are connected if you can get to the endnode starting in an intermediate node, and you can reach that intermediate node by using an edge from the startnode. The simplest case is if the start and endnode are connected by just an edge.
Now imagine the following query:
   brussels path: ?to
If we resolve this query using SLD resolution we would get into an infinite computation. The head of the first rule unifies with our query, so we resolve the conditions of that rule. The first condition is ?from path: ?somewhere, which becomes brussels path: ?somewhere after variable substitution. This is the same query we are actually resolving, upto variable renaming, resulting in an infinite computation.
This is where SLG resolution differs from SLD resolution. SLG resolution will detect we are already resolving the same query, and will suspend the current rule. It will then try other rules that match, in our case this is the second rule for path. After resolving that rule we return our answers to the previously suspended rule. This rule can then continue with new bindings, no longer yielding an infinite computation.
In general we get the same results with SLG resolution as with SLD resolution, but there are cases where SLG resolution can provide us with answers where SLD resolution would fail. There is a downside, as SLG resolution has more overhead than SLD resolution, as we have to keep track of rules we are currently evaluating.
For more information regarding tabled resolution and the implementation we refer to the following papers:
1) Tabled Evaluation with Delaying for General Logic Programs, Weidong Chen, David S. Warren
2) Implementation of Tabled Evaluation with Delaying in Prolog, R. Ramesh, Weidon ChenBesides SLD resolution SOUL also features SLG resolution, also known as tabled resolution. The following program will illustrate the advantages of SLG resolution:
tabled ?from path: ?to if
  ?from path: ?somewhere,
  ?somewhere edge: ?to
 
tabled ?from path: ?to if
  ?from edge: ?to

This is a simple way to define a path in a graph between two nodes. Two nodes are connected if you can get to the endnode starting in an intermediate node, and you can reach that intermediate node by using an edge from the startnode. The simplest case is if the start and endnode are connected by just an edge.

Now imagine the following query:

brussels path: ?to

If we resolve this query using SLD resolution we would get into an infinite computation. The head of the first rule unifies with our query, so we resolve the conditions of that rule. The first condition is ?from path: ?somewhere, which becomes brussels path: ?somewhere after variable substitution. This is the same query we are actually resolving, upto variable renaming, resulting in an infinite computation.

This is where SLG resolution differs from SLD resolution. SLG resolution will detect we are already resolving the same query, and will suspend the current rule. It will then try other rules that match, in our case this is the second rule for path. After resolving that rule we return our answers to the previously suspended rule. This rule can then continue with new bindings, no longer yielding an infinite computation.

In general we get the same results with SLG resolution as with SLD resolution, but there are cases where SLG resolution can provide us with answers where SLD resolution would fail. There is a downside, as SLG resolution has more overhead than SLD resolution, as we have to keep track of rules we are currently evaluating.

In SOUL you can mark a rule with the prefix tabled to use SLG resolution. You can use it like any other normal rule. Behind the scenes SOUL will transform the rule to the corresponding SLG program.

For more information regarding tabled resolution and the implementation we refer to the following papers:

  1. Tabled Evaluation with Delaying for General Logic Programs, Weidong Chen, David S. Warren
  2. Implementation of Tabled Evaluation with Delaying in Prolog, R. Ramesh, Weidon Chen