MVILAIN@G.BBN.COM.UUCP (10/27/87)
BBN Science Development Program
AI Seminar Series Lecture
DEPENDENCY DIRECTED PROLOG
Jeffrey Mark Siskind
MIT Laboratory for Computer Science
(also: summer intern at Xerox PARC)
(Qobi@ZERMATT.LCS.MIT.EDU)
BBN Labs
10 Moulton Street
2nd floor large conference room
10:30 am, Tuesday November 3
In this talk I will describe an implementation of pure Prolog which uses
dependency directed backtracking as a control strategy for pruning the
search space. The implementation uses a strategy whereby the Prolog
program is compiled into a finite set of templates which characterize a
potentially infinite boolean expression which is satisfiable iff there
is a proof of the goal query. These templates are incrementally
unraveled into a sequence of propositional CNF SAT problems and
represented in a TMS which is used to find solutions using dependency
directed backtracking. The technique can be extended to use ATMS-like
strategies for searching for multiple solutions simultaneously.
Two different strategies have been implemented for dealing with
unification. The first compiles the unification constraints into SAT
clauses and integrates them in the TMS along with the and/or goal tree
produced by unraveling the templates. The second uses a separate module
for doing unification at run time. This unifier is novel in that it
records dependencies and allows nonchronological retraction. The
interface protocol between the TMS and the unifier module has been
generalized to allow integration of other "domains" of predicates, such
as linear arithmetic and simple linear inequalities, to be built into
the system while still preserving the soundness and completeness of the
pure logical interpretation of Prolog.
In the talk, time permitting, I will discuss the search prunning
advantages of this approach and its relation to previous approaches, the
implementation mechanism, and some recent work indicating the potential
applicability of this approach to parsing with disjunctive feature
structures, such as done with the LFG and related grammar formalisms.
-------