|
|
|
Logic Programming Research Group
Research Group at the University of Kent
Andy King and Aliy Fowler
University of Kent
UK
|
|
Editor: Enrico Pontelli
|
Logic programs describe relations and therefore are potentially
reversible. Yet, rather annoyingly, logic programs often fail to
terminate when used in reverse mode. We have addressed this problem by
automatically deriving the control for logic programs by reasoning about
the depth of derivations. Our scheme derives delay declarations, which
orchestrate the control and permit the program to the used in any mode
without compromising termination [Fundamenta Informaticae, 69(1-2): 2006].
To support this scheme, it is necessary to know about how the depth of
derivations relates to the size of arguments. Another theme of our work
has therefore been developing analyses that reason about the relative
sizes of arguments using systems of linear constraints [TPLP, 5(1-2):
2005]. The key idea in this work is to reason about a constraint such as
X = f(Y) with another constraint X = 1 + Y that expresses the relative
sizes of X and Y.
Using constraints to reason about constraints is an important idea in
logic programming, and in this vein we have deployed propositional
constraints [TPLP, 3(1): 2003] to infer when a variable in a program is
completely instantiated (ground). We have also used propositional
constraints (represented using tree data-structures known as ROBDDs) to
compactly describe global constraints [TACAS, 2006].
Much of this work finds application in checking the correctness of logic
programs. Given a logic program and description of a class of query,
one might naturally ask whether the program can violate an assertion, or
fall into an infinite loop, or in concurrency is used, drop into a state
that includes a process, which suspends indefinitely. These verification
problems can all be reversed, that is, rather than ask if a given class
of query is guaranteed to satisfy some correctness criterion, one may
instead wish to derive the class of query that is certifiably correct.
The reversed form of verification is attractive because the user merely
has to point the verifier at a program and then check whether the class
of query inferred conforms to their expectations. If not, then the
program is potentially buggy. This technique has been used to locate,
among other things, concurrency [ACM ToCL, to appear] and determinacy
faults [ESOP, 2005].
Apart from our work on the logic programming paradigm itself, we are
using logic programming to support second language learning -
specifically to produce sophisticated answer-checking algorithms for
CALL, based on sequence comparison rather than parsing. Sequence
comparison has been successfully used in fields such as molecular
biology, gas chromatography and speech recognition, but has rarely been
applied in any rigorous way to CALL. Calculating edit distance between
DNA sequences, chromatograms or soundwave patterns involves identifying
substitutions, insertions, deletions, transpositions of adjacent
elements (and in some cases compressions and expansions). However real
complexity comes from factoring in re-ordering of the basic elements
within the sequence, as can occur with malformed natural language
strings. Using logic programming to build enhanced sequence comparison
techniques for error detection allows CALL systems to give useful
feedback, without the need to build language-specific parsers (which can
fail when errors in user-input are too numerous). It also removes the
need to establish answer equivalence as a separate (and often not very
successful) stage [CALL & Monitoring the Learner, 2006].
Research is collaborative venture and much of the work described in this
spotlight article is joint with: Samir Genaim, Lunjin Lu, Jonathan
Martin, Florence Benoy, Jan Georg-Smaus, Jacob Howe, Axel Simon, Neil
Kettle and Tadeusz Strzemecki. We would like to thank our co-authors and
colleagues for providing an environment where logic programming has been
able to grow and blossom.
Andy King and Aliy Fowler, October, 2007
|