liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
A comparison of SL- and unit-resolution search rules for stratified logic programs
Linköping University, Department of Computer and Information Science, TCSLAB - Theoretical Computer Science Laboratory.
2010 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
Abstract [en]

There are two symmetrical resolution rules applicable to logic programs - SL-resolution which yields a top-down refutation and unit-resolution which yields a bottom-up refutation. Both resolution principles need to be coupled with a search rule before they can be used in practice. The search rule determines in which order program clauses are used in the refutation and affects both performance, completeness and quality of solutions. The thesis surveys exhaustive and heuristic search rules for SL-resolution and transformation techniques for (general) logic programs that makes unit-resolution goal oriented.

The search rules were implemented as meta-interpreters for Prolog and were benchmarked on a suite of programs incorporating both deterministic and nondeterministic code. Whenever deemed applicable benchmark programs were permuted with respect to clause and goal ordering to see if it affected the interpreters performance and termination.

With the help of the evaluation the conclusion was that alternative search rules for SL-resolution should not be used for performance gains but can in some cases greatly improve the quality of solutions, e.g. in planning or other applications where the quality of an answer correlates with the length of the refutation. It was also established that A* is more flexible than exhaustive search rules since its behavior can be fine-tuned with weighting, and can in some cases be more efficient than both iterative deepening and breadth-first search. The bottom-up interpreter based on unit-resolution and magic transformation had several advantages over the top-down interpreters. Notably for programs where subgoals are recomputed many times. The great disparity in implementation techniques made direct performance comparisons hard however, and it is not clear if even an optimized bottom-up interpreter is competitive against a top-down interpreter with tabling of answers.

Place, publisher, year, edition, pages
2010. , 70 p.
Keyword [en]
logic programming, search rule, resolution, prolog, heuristic search
National Category
Computer Science
URN: urn:nbn:se:liu:diva-57363ISRN: LIU-IDA/LITH-EX-G--10/013--SEOAI: diva2:325247
2010-06-08, Donald Knuth, Linköping, 20:32 (Swedish)
Available from: 2010-06-18 Created: 2010-06-17 Last updated: 2010-06-28Bibliographically approved

Open Access in DiVA

A comparison of SL- and unit-resolution search rules for stratified logic programs(625 kB)431 downloads
File information
File name FULLTEXT01.pdfFile size 625 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Lagerqvist, Victor
By organisation
TCSLAB - Theoretical Computer Science Laboratory
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 431 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 6456 hits
ReferencesLink to record
Permanent link

Direct link