Interpolation in propositional Horn logic

In this paper we give an abstract representation of propositional Horn logic (finite or infinitary) in terms of set-valued functions F : (sic) (PR) -> (sic) (PR); here PR is the collection of atomic propositions. We investigate the properties of set-valued functions and establish that they satisfy the axioms of weak lazy Kleene algebra. These axioms and other properties are used to prove uniform left interpolation for propositional Horn logic. Then we introduce thin set-valued functions, which enable us to prove polynomial interpolation for propositional Horn logic. For the infinite case, the Axiom of Choice is used.