Some Model Theoretical Results over Horn Formula

摘要

Horn clause plays a basic role in logic programming and are important for many constructive logics. Interpolation theorem is also an important topic for many monotonic or non-monotonic logic systems. The interpolation theorem for Horn clauses under the derivability from their proof theory was formulated by Gabby and Maksimova. Using model theoretical methods, this paper demonstrates the following results for Horn clauses under the classical propositional derivability. First we formulate that the restrict over a sub-language of a close set of Horn formulas is logically equivalent to a set of Horn formulas. Next the interpolation theorem and the parallel interpolation theorem over Horn formulas under classical propositional derivability was formulated. The paper answers partially the open problem proposed by Kourousias and Makinson in 2007.