with partial functions. A sound system for Horn logic with partial

functions, called PHL (investigated by E. Palmgren and S. Vickers), is

one of many alternative systems. In this talk, we simplify and extend

PHL to handle, not only partial, but also lazy functions.

The system is given semantics in a way that stays very close to the

traditional universal algebra semantics for equational logic, and both

soundness and completeness is shown. Further, some proof theoretic

properties of the new system, particularly regarding the substitution and

cut rules, are investigated. Finally its precise relation to PHL is

clarified by means of intertranslatability results.

Robert Recorde Room

Department of Computer Science