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

Direct link
Improving goal directed bottom-up evaluation of logic programs
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
(English)Manuscript (preprint) (Other academic)
Abstract [en]

This paper introduces a new strategy for goal directed bottom-up evaluation of logic programs. The strategy is based on a combination of two known techniques: dividing a program into strongly connected components (SCC) and Induced Magic-sets.

In our approach no magic transformation is needed (as in Induced Magic-sets). We introduce a notion of a call-success dependency graph that constructed directly from the original program. Its SCCs are used to optimize a fixpoint computation (i.e. they coincide with SCCs of a corresponding magic program). The new graph contains substantially fewer edges than standard dependency graph of a magic program, and thus its SCCs are computed faster. We also show how to incorporate SCC-based optimization into the Unduced Magic-sets technique. This is achived by modifying the basic Induced Magic method, so that the fixpoints are computed locally for every SCC.

The impact of our method is illustrated by experimental results.

Keyword [en]
magic-sets, bottom-up evaluation
National Category
Engineering and Technology
URN: urn:nbn:se:liu:diva-87997OAI: diva2:601007
Available from: 2013-01-28 Created: 2013-01-28 Last updated: 2013-01-28
In thesis
1. A type-based framework for locating errors in constraint logic programs
Open this publication in new window or tab >>A type-based framework for locating errors in constraint logic programs
2002 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

This thesis presents a method for automatic location of type errors in constraint logic programs (CLP) and a prototype debugging tool. The appriach is based on techniques of verification and static analysis iriginating from logic programming, which are substantially extended in the thesis. The main idea is to verify partial correctness of a program with respect to a given specification which is intended to describe (an approximation of) the call-success semantics of the program. This kind of specification, describing calls and successes for every predicate of a program is known as descriptive directional type. For specifying types for CLP programs the thesis extends the formalism of regular discriminative types with constraint-domain-specific base types and with parametric polymorphism.

Errors are located by identifying program points that violate verification conditions for a given type specification. The Specifications may be developed interactively taking into account the results of static analysis.

The main contributions of the thesis are:

  • a verification method for proving partial correctness of CLP programs with respect to polymorphic spicifications of the call-success semantics,
  • a specification language for defining parametric regular types,
  • a verification-based method for locating errors in CLP programs,
  • a static analysis method for CLP which is an adaptation and generalization of techniques previously devised for logic programming; its implementation is used in our diagnosis tool for synthesizing draft specifications,
  • an implementation of the prototype diagnosis tool (called TELL).

Place, publisher, year, edition, pages
Linköping: Linköpings universitet, 2002. 22 p.
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 772
National Category
Computer Science
urn:nbn:se:liu:diva-35577 (URN)27725 (Local ID)91-7373-422-5 (ISBN)27725 (Archive number)27725 (OAI)
Public defence
2002-09-13, Estraden seminarierum, Hus E, Linköpings universitet, Linköping, 13:15 (Swedish)
Available from: 2009-10-10 Created: 2009-10-10 Last updated: 2013-01-28

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Pietrzak, Pawel
By organisation
Department of Computer and Information ScienceThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
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: 59 hits
ReferencesLink to record
Permanent link

Direct link