%{ 
The operational semantics of Twelf are similar to those of Prolog, 
a style known as ''backward chaining'' or ''goal-directed'' proof 
search. '''Tabled logic programming''', which uses Twelf's 
<tt>[[%tabled]]</tt> and <tt>[[%querytabled]]</tt> directives to 
allow Twelf to prove theorems that might be time-consuming or 
impossible to prove otherwise. The tabled logic programming 
capabilities are a 
part of Twelf's capabilities as a logical framework, but not as a 
metalogical framework; in other worlds, tabled logic programming 
cannot be used to prove [[metatheorems]].

[[Image:Searchgraph-found.svg|thumb|right|325px|The graph used in this example, and the path that the tabled logic query finds to get from node a to node g.]] 

The simplest examples of the power of tabled logic programming in 
practice involve judgments that involve transitive and/or symmetric 
closures, such as searching for a path in a graph or formalizing a 
language with subtyping. Using standard backward-chaining proof search, 
it is almost impossible to write terminating programs that search for 
paths, and using backward-chaining search for subtyping typically 
requires a separate definition of "algorithmic subtyping" that must 
be shown to be sound and complete with respect to the clearer, simpler 
definition of subtyping that uses transitivity.

This article will use as its example a path-finding algorithm 
on an undirected graphs. 

}%

%{ == Defining the graph == }%

%{ === Nodes === }%

node : type.

a : node.
b : node.
c : node.
d : node.
e : node.
f : node.
g : node.
h : node.

%{ === Edges === }%

%{ While we will consider edges in our graph to be undirected, 
we will only define the edge in one, arbitrary, direction. }%

edge : node -> node -> type.

ab : edge a b.
ac : edge a c. 
bc : edge b c.
bd : edge b d.
cd : edge c d.
ce : edge c e.
de : edge d e.
df : edge d f.
fg : edge f g.

%{ === Paths in the graph === }%

%{
This is normally where we would get into trouble; in standard 
logic programming, it is difficult if not impossible to avoid 
non-terminating behavior when writing a judgment defining a 
transitive-symmetric closure like <tt>path</tt>. However, by 
adding the directive <tt>[[%tabled]] path</tt>, we will be able 
to use <tt>[[%querytabled]]</tt> directives to cause each instance 
of <tt>path A B</tt> to be derived at most once during the course 
of a search: the result is a query that terminates rapidly, 
instead of not at all.
}%

path : node -> node -> type.
%tabled path.

path/link : edge A B -> path A B.
path/refl : path A B -> path B A.
path/trans : path A B -> path B C -> path A C.

%{ == Searching the graph == }%

%{ 
It is crucial that we use <tt>[[%querytabled]]</tt> rather than 
<tt>[[%query]]</tt> in our queries if we wish for them to terminate. 
Even though we ask Twelf for as many solutions as it can find, the 
tabled proof search ensures that we can only find one proof of any 
given path, and the path that is found is by not necessarily the shortest.
While the path that is found is shown on the graph above, the edge <tt>ab</tt>
actually appears three times here - if we use parenthesis to show the order in which
tabled search connected paths, the path that is found is
<tt>a</tt> - ((<tt>b</tt> - ((<tt>a</tt> - <tt>b</tt> - <tt>d</tt>) - <tt>f</tt>)) 
- <tt>g</tt>).
|check=decl noinclude=true}%

%querytabled * * D : path a g.

%{
We can also run a terminating search for a path that does not exist, 
such as one from <tt>a</tt> to <tt>h</tt>.
|check=decl noinclude=true}%

%querytabled * * D : path a h.

%.

== See also ==

* <tt>[[%tabled]]</tt>
* <tt>[[%querytabled]]</tt>
* {{guide|chapter=5|section=31|title=Tabled Logic Programming}}