The Logical Structure of Sequential Prolog

James H. Andrews

Abstract: Previous logical characterisations of sequential Prolog have not dealt with questions of completeness, and therefore have not adequately described termination. Denotational characterisations deal with termination properly, but do so in a very functional, non-logical manner. This paper presents sound, complete, and logical characterisations of pure sequential Prolog with which termination and correctness properties of programs can be proved. These characterisations affirm that sequential Prolog has a logical structure and is a fully valid part of the logic programming paradigm.

LFCS report ECS-LFCS-90-110

Previous | Index | Next