A constructive view of PROLOG

AbstractA constructive rationalization of PROLOG is presented, covering the logical form of definite clause programs and the role of negative (goal) clauses. This view is developed from the idea, taken from set theory, that a constructive theory can be obtained if classical reasoning is confined to a constructively limited basis. The syntax of definite clauses is seen as reflecting a constructive view of description in that it prevents the expression of incomplete and negative information; the purely negative clauses initiate a classical proof technique, operating on a definite axiomatic basis