GCLA II. A definitional approach to control

This paper describes the logic programming language GCLA II, its operational semantics and parts of its theortical foundations. GCLA II is a generalization of the language GCLA (Generalized Horn Clause Language) argumented by a method to guide and constrain proof search. The method is based on specification of strategies in a meta language that is a sub language of GCLA itself. A GCLA II program is partioned into two distinct parts. One is used to express the declarative content of the program, while the other is used to define the possible inference made from this declarative knowledge. Altough the intended use of the declarative part and the procedural parts are quite different, they can both be described in the formalism of partial inductive definitions. Thus we preserve a declarative reading of the program as a whole. In particular, given certain sythactic constraints on the program, the heuristics associated with proof search does not affect the declarative reading of the declarative part of the program at all. Several experiments intepreters and a compiler from GCLA II to Prolog have been implemented