DECLARATIVE SEMANTICS OF LOGICAL READ-ONLY VARIABLES.

The authors consider the declarative (model-theoretic and fixed-point) semantics of Horn clause logic with read-only variables. The logic language considered is Concurrent Prolog without the commit operator. The results can be considered as a first step toward a mathematical characterization of Concurrent Prolog programs. The declarative semantics proposed is equivalent to the operational semantics and is based on a new notion of Herbrand interpretation, which allows one to characterize values which can only be consumed. A slight extension of Concurrent Prolog read-only variables is first considered. The variables are easier to handle from the semantics viewpoint and still have synchronization power. The model construction is then sketched for the Concurrent Prolog case.