Inductive assertion method for logic pograms
type: Item
instance of: scholarly article
title: Inductive assertion method for logic pograms
zbMATH Open document ID: 0648.68019
DOI: 10.1016/0304-3975(88)90099-0
author: Włodzimierz Drabent
author: Jan Maluszyński
published in: Theoretical Computer Science
publication date: 1988-01-01T00:00:00Z
review text: Certain properties of logic programs are inexpressible in terms of their declarative semantics. One example of such properties would be the actual form of procedure calls and successes which occur during computations of a program. They are often used by programmers in their informal reasoning. In this paper, the inductive assertion method for proving partial correctness of logic programs is introduced and proved sound. The method makes it possible to formulate and prove properties which are inexpressible in terms of the declarative semantics. An execution mechanism using the Prolog computation rule and arbitrary search strategy (e.g., OR-parallelism or Prolog backtracking) is assumed. The method may also be used to specify the semantics of some extra-logical built-in procedures for which the declarative semantics is not applicable.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4058827
zbMATH Keywords: logic programs
zbMATH Keywords: inductive assertion method
zbMATH Keywords: partial correctness
zbMATH Keywords: declarative semantics
zbMATH Keywords: Prolog
zbMATH Keywords: OR-parallelism
zbMATH Keywords: backtracking
MaRDI profile type: Publication
full work available at URL: 0304-3975(88)90099-0
OpenAlex ID: W2118483018
cites work: Contributions to the Theory of Logic Programming
cites work: Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
cites work: Relating logic programs and attribute grammars
cites work: Q3776674
cites work: Q5584402
cites work: Q3698285
cites work: An axiomatic basis for computer programming
cites work: Derivation of Logic Programs
cites work: Q3339245
cites work: Q3995530
cites work: Some global optimizations for a PROLOG compiler
cites work: A language of specified programs
description: scientific article; zbMATH DE number 4058827