00001 <!doctype html public "-//w3c//dtd html 4.0 transitional//en">
00002 <html>
00003 <head>
00004 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
00005 <meta name="GENERATOR" content="Mozilla/4.61 [en] (X11; I; Linux 2.2.12-32 i686) [Netscape]">
00006 <title>The XSB Research Group</title>
00007 </head>
00008 <body>
00009 <img SRC="new.gif" ALT="" IMG align=TOP><font color="#FF0000">XSB
00010 2.3</font> has now been released!
00011 <p>
00012 <hr>
00013 <h2>
00014 The XSB Research Group</h2>
00015 The focus of the XSB research group is the development and application
00016 of the XSB system, an open source logic programming system that extends
00017 Prolog with new semantic and operational features, mostly based on the
00018 use of Tabled Logic Programming or <i>tabling.</i>
00019 <p>At first, tabling may seem like a simple idea. At a very high level,
00020 during computation of a goal to a logic program, each subgoal <i>S</i>
00021 is registered in a table the first time it is called, and unique answers
00022 to <i>S </i>are added to the table as they are derived. When subsequent
00023 calls are made to<i> S</i>, the evaluation ensures that answers to <i>S
00024 </i>are
00025 read from the table rather than being rederived using program clauses.
00026 Even from this simple description, a first advantage of tabling can be
00027 seen, that it provides termination to various classes of programs. Consider
00028 the case of ground positive datalog programs ---i .e.Horn Clause programs
00029 that allow only constant terms over a finite alphabet. Such a program contains
00030 only finitely many ground atoms. Each of these atoms can be added at most
00031 once to the table as a subgoal, and each such subgoal can have at most
00032 one answer, leading to a finite computation. Tabled logic programming for
00033 Horn clause programs was first formalized in the early 1980's. Additionally,
00034 several formalisms and systems have been based both on tabled resolution
00035 and on magic sets, which can also be seen as a form of tabled logic programming.
00036 <p>However, tabling can be used to far greater effect than ensuring termination
00037 for Horn clause programs. Seen abstractly, the table described above represents
00038 selected global elements of a given state of a computation, in this case,
00039 subgoals called and their answers so far derived. One powerful feature
00040 of tabling is its ability to maintain other global elements of a computation
00041 in the ``table,'' such as information about whether one subgoal depends
00042 on another, and whether the dependency is through negation. By maintaining
00043 this global information, tabling can be used to evaluate normal logic programs
00044 under the <i>Well-Founded Semantics (WFS).</i> While computation of the
00045 well-founded semantics using tabling is quite complex, the essential idea
00046 is that global information about dependencies is used to determine the
00047 truth value of literals that do not have a derivation. If such literals
00048 are involved in a cyclic dependency through negation, they are undefined
00049 under WFS; if not, the literals belong to an unfounded setand are false
00050 in WFS. In fact, it can be shown that tabling allows non-floundering datalog
00051 programs with negation to terminate with polynomial data complexity under
00052 the well-founded semantics. A second feature to extend the power of tabling
00053 is called <i>tabled aggregation</i>. If <i>partial order tabled aggregation</i>
00054 is used, relations can be defined on answers in a table such that only
00055 those which are optimal with respect to the partial order need be retained.
00056 If <i>functional tabled aggregation</i>} is used, functions can be defined
00057 on answers to a subgoal in a table so that an associative function~---~say
00058 a maximum or least upper bound~---~of the answers is retained rather than
00059 the set of answers themselves.
00060 <p>Using these features, XSB can serve as a development platform for applications
00061 in two ways. First, applications can be programmed using normal program
00062 clauses and the libraries of XSB. Second, XSB can serve as the implementational
00063 infrastructure for useful logics which then serve as the programming language
00064 for applications. These two choices can be thought of as extremes, and
00065 most applications so far have used a mixture of the two approaches.
00066 <p>We consider first the logics that have been implemented in XSB. Based
00067 on XSB's implementation of WFS, the Well-Founded Semantics with Explicit
00068 Negation (WFSX) has been implemented and extended to allow abduction and
00069 logical program updates; the object-based Frame Logic (F-Logic) and several
00070 temporal concurrency logics including the Modal <b><i><u>mu</u></i></b>-Calculus
00071 and Concurrent Temporal Logic have also been implemented using WFS, as
00072 described below. Using functional tabled aggregation, Generalized Annotated
00073 Programs and a type of probabilistic logic programs have been implemented;
00074 while using partial order tabled aggregation a species of Preference Logic
00075 has been implemented. Many of these logics will become more powerful with
00076 the recent addition of logical constraint handling techniques to XSB.
00077 <p>Before turning to applications of these logics we consider in detail
00078 how XSB can form the underpinnings of a system based on a non-traditional
00079 logical formalism using the case of FLORA, which which amalgamates F-logic,
00080 Transaction Logic, and HiLog, and is implemented as an optimizing compiler
00081 whose target code is a normal program executable by XSB. Consider an F-logic
00082 term:
00083 <ul>
00084 <li>
00085 <b>john[spouse->mary, child->>{bob,bill}]</b></li>
00086 </ul>
00087 which indicates that the object <b>john </b>has a spouse-attribute
00088 of <b>mary</b> and chidren-attributes<b> bob</b> and <b>bill</b>. This
00089 term is translated into a conjunction of triples:
00090 <ul>
00091 <li>
00092 <b>fd(john,spouse,mary)</b></li>
00093
00094 <li>
00095 <b>mvd(john,child,bob)</b></li>
00096
00097 <li>
00098 <b>mvd(john,child,bill)</b></li>
00099 </ul>
00100 While this plan seems straightforward, it is hard to realize in a standard
00101 Prolog framework. The main reason is that the translation into XSB uses
00102 only a small number of predicates, which leads to two main problems: (1)
00103 The loss of indexing; and (2) Termination problems.
00104 <p>The first problem cannot be easily solved by increasing the number of
00105 predicates, because of the meta-programming features of F-logic. However,
00106 FLORA takes advantage of the various optimization techniques that exist
00107 in XSB, such as <i>specialization</i> and <i>unification factoring</i>.
00108 The second problem is more serious: the small number of predicates used
00109 in the translation makes even non-recursive FLORA programs into highly
00110 recursive XSB programs. In this situation it is hard to build a compiler
00111 that would produce programs with reasonable termination behavior without
00112 tabling.
00113 <p>The profusion of logics implementable in XSB has led to a proliferation
00114 of research and commercial applications, many of them in areas in which
00115 logic programming has not previously been successful. Using XSB, WFSX has
00116 been used for machine learning. With the addition of abduction, WFSX has
00117 been used for psychiatric diagnosis, as well as for fault diagnosis in
00118 electronic circuits. FLORA has been used for the creation of Web agents,
00119 for applications in neuroscience, and for processing ontologies and meta-data.
00120 Probabilistic logic programs have been used to allow mined association
00121 rules to be used within an intensional database. Preference Logic Programs
00122 have been used to for data cleaning through the formalism of Preference
00123 Logic Grammars. These applications typically mix the use of the various
00124 logics with traditional Prolog programming techniques. The reasons for
00125 the success of each application varies. However, the use of XSB for the
00126 verification of concurrent systems, or <i>model-checking</i> illustrates
00127 many common features of these applications.
00128 <p>Model checkers are usually formulated in two stages. First there is
00129 a <i>process logic</i>, representing the interaction of communicating systems.
00130 Common process logics are Milner's CCS (Calculus for Communicating Systems)
00131 and the \pi-calculus. Abstractly, a process logic can be seen as a labelled
00132 transition system consisting of a set <i>S</i> of global system states
00133 and a labelled relation among elements of <i>S </i>representing communications
00134 among the systems or changes in the internal state of these systems. Transition
00135 systems generated by process logics contain loops and so require a mechanism
00136 like tabling even to be traversed. Temporal concurrency logics, such as
00137 the Modal- \mu-calculus and CTL* have been designed in order to be able
00138 to query interesting properties of transition systems such as whether termination
00139 occurs along all paths starting from a given state, whether such paths
00140 are free from deadlock, are fair, and so on. It can be shown that many
00141 concurrent temporal logics --- such as the non-alternating modal \mu-calculus
00142 --- can be embedded into <i>dynamically</i> <i>stratified</i> logic programs,
00143 and can be evaluated directly in XSB producing a two-valued well-founded
00144 model. It is unknown whether general concurrent temporal logics, (such
00145 as the alternating modal \mu-calculus) can be modularly embedded into the
00146 well-founded semantics, but such logics have been evaluated by using XSB
00147 as a preprocessor to a stable model generator. Thus in model checking,
00148 XSB may be used alone or with other tools depending on the needs of the
00149 user. Given its power and applicability, it has not been trivial to implement
00150 tabling so that it is both efficient and integrable with Prolog. Much of
00151 the work of the XSB group has involved design and implementation of its
00152 underlying engine, the SLG-WAM, and its extensions. From the point of view
00153 of implementation, tabling has necessitated the development of algorithms
00154 in a variety of areas. During a tabled evaluation, one computation path
00155 may consume answers produced by another computation path. This means that
00156 resources must be retained for environments that consume answers to a given
00157 subgoal until they have consumed all answer that the evaluation will produce
00158 for that subgoal. Furthermore, the evaluation must be able to switch efficiently
00159 between computation paths that produce answers and those that consume them.
00160 These differences between tabled and non-tabled evaluation have led to
00161 the study of strategies to schedule the return of answers to consuming
00162 environments; the study of how to efficiently determine when mutually recursive
00163 sets of subgoals have been completely evaluated; and of how to perform
00164 efficient memory management, environment switching and garbage collection.
00165 Much work has also been done on how to efficiently access tables from a
00166 WAM-style engine, how to maintain dependency information in the table (and
00167 stacks) for the well-founded semantics, and how answers in a table can
00168 be efficiently shared among subsuming calls.
00169 <p>Descriptions of tabling algorithms their implementations; of implemented
00170 logics, their applications, and implementations can be found via
00171 <ul>
00172 <li>
00173 <a href="xsb-people.html">List of people</a></li>
00174 </ul>
00175
00176 <p><br><a href="http://sourceforge.net"><img SRC="sflogo.php" ALT="SourceForge Logo" BORDER=0 height=31 width=88></a>
00177 </body>
00178 </html>
