COMPLETE SEMANTIC CHARACTERIZATION OF K-LEAF, A LOGIC LANGUAGE WITH PARTIAL FUNCTIONS.

A definition is given of the experimental first-order logic and functional language K-LEAF, based on Horn-clause logic with equality. A novel aspect of the language with respect to similar proposals (e. g. the earlier language LEAF) is the development of a model-theoretic semantics explicitly taking into account partial functions, and which the operational semantics (based on flattening and outermost resolution) has been proved sound and complete. This makes it possible to cope with nonterminating functions and infinite data structures in a nice and natural framework. The rationale behind the design choice and a framing of them in the more general setting of inference systems for Horn-clause logic with (directed) equality are presented.