Lifting Transformations

Abstract

Lifting is a well-known technique in resolution theorem proving, logic programming, and term rewriting. In this paper, the authors formulate lifting as an efficiency-motivated program transformation applicable to a wide variety of nondeterministic procedures. This formulation allows the immediate lifting of complex procedures, such as the Davis-Putnam algorithm, which are otherwise difficult to lift. They treat both classical lifting, which is based on unification, and various closely related program transformations that they also call lifting transformations. These nonclassical lifting transformations are closely related to constraint techniques in logic programming, resolution, and term rewriting. Formulating these techniques as transformations on nondeterministic programs expands the range of procedures to which the techniques can be easily applied.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1991
Accession Number
ADA259672

Entities

People

  • David A. Mcallester
  • Jeffrey Mark Siskind

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Artificial Intelligence
  • Artificial Intelligence Computing
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Efficiency
  • Language
  • Lisp Programming Language
  • Programming Languages
  • Standards

Fields of Study

  • Engineering

Readers

  • Aerodynamics/Aeronautics.
  • Computational Linguistics
  • Theoretical Analysis.