Amazon cover image
Image from Amazon.com

Termination proofs for logic programs / Lutz Plümer.

By: Material type: TextTextSeries: Lecture notes in computer science ; 446. | Lecture notes in computer science. Lecture notes in artificial intelligence.Publisher: Berlin ; New York : Springer-Verlag, ©1990Description: 1 online resource (viii, 142 pages) : illustrationsContent type:
  • text
Media type:
  • computer
Carrier type:
  • online resource
ISBN:
  • 9783540471639
  • 3540471634
Subject(s): Additional physical formats: Print version:: Termination proofs for logic programs.DDC classification:
  • 006.3 20
LOC classification:
  • QA76.63 .P58 1990
Other classification:
  • 54.51
Online resources:
Contents:
Basic notions -- Static program properties and transformations -- Terminating logic programs -- The problem of local variables -- And/or dataflow graphs -- A termination proof procedure -- Integration of unfolding techniques -- Conclusions.
Action note:
  • digitized 2010 HathiTrust Digital Library committed to preserve
Summary: Termination proofs constitute a crucial part of program verification. Much research about termination has been done in the context of term rewriting systems. But until now there was little hope that termination proofs for nontrivial programs could be achieved automatically. This book gives a comprehensive discussion of the termination problem in the context of logic programming. Although logic programs pose special difficulties for termination proofs it turns out that automation of this task is obtainable to a much larger degree than for programs in imperative languages. A technique for the automatic derivation of termination proofs is presented in detail. The discussion of several nontrivial examples illustrates its range of applicability. The approach is based on the concept of declarative semantics, and thus makes use of an important feature of logic programming.
Holdings
Item type Current library Collection Call number Status Date due Barcode Item holds
eBook eBook e-Library eBook LNCS Available
Total holds: 0

Includes bibliographical references (pages 132-139) and index.

Use copy Restrictions unspecified star MiAaHDL

Electronic reproduction. [Place of publication not identified] : HathiTrust Digital Library, 2010. MiAaHDL

Master and use copy. Digital master created according to Benchmark for Faithful Digital Reproductions of Monographs and Serials, Version 1. Digital Library Federation, December 2002. MiAaHDL

http://purl.oclc.org/DLF/benchrepro0212

digitized 2010 HathiTrust Digital Library committed to preserve pda MiAaHDL

Termination proofs constitute a crucial part of program verification. Much research about termination has been done in the context of term rewriting systems. But until now there was little hope that termination proofs for nontrivial programs could be achieved automatically. This book gives a comprehensive discussion of the termination problem in the context of logic programming. Although logic programs pose special difficulties for termination proofs it turns out that automation of this task is obtainable to a much larger degree than for programs in imperative languages. A technique for the automatic derivation of termination proofs is presented in detail. The discussion of several nontrivial examples illustrates its range of applicability. The approach is based on the concept of declarative semantics, and thus makes use of an important feature of logic programming.

Print version record.

Basic notions -- Static program properties and transformations -- Terminating logic programs -- The problem of local variables -- And/or dataflow graphs -- A termination proof procedure -- Integration of unfolding techniques -- Conclusions.

Powered by Koha