Interpolation in propositional Horn logic

Gerard R. Renardel De Lavalette*

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review


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.

Original languageEnglish
Pages (from-to)1189-1215
Number of pages27
JournalJournal of Logic and Computation
Issue number6
Publication statusPublished - Sep-2018


  • propositional Horn logic
  • uniform interpolation
  • polynomial interpolation
  • lazy Kleene algebra

Cite this