How are prime implicates of HORN-Formulas defined?

Question

I'm confused about the definition of prime implicates in Horn formulas.

For example in the paper of Kira 2012 on page 109 it is stated:

Now in the paper of Boros 2010 on page 82 the following definition is used:

My goal is to decide whether a Horn formula is prime or not in polynomial time. For that I want to assume the definition used in Kira 2012.

How can I prove that the two definitions above for prime implications of Horn formulas are equivalent?

Edit: What I have so far is that if we assume Kiras definition and have for example a clause $C=\neg x_1 \vee \neg x_2 \vee x_3$ of formula $F$ and $C$ is prime then $F\rightarrow C$. If one neglects a literal in C we get $C_1=\neg x_1 \vee \neg x_2$ and obviously $C_1 \rightarrow C$. Therefore, since $C$ is prime then by Kiras definition no other proper sub-clause of $C$ is an implicant so $F \nrightarrow C_1$. Neglecting more literals in $C_1$ to get $C_2$ will give $C_2\rightarrow C_1 \rightarrow C$. Then by definition of $C$ it must be that $F\nrightarrow C_2 \rightarrow C_1$ and we get that all sub-clauses of $C_1$ are not prime if we check that $C_1$ is not prime. Therefore, to check if a Formula $F$ is prime we consider each clause $C$ and neglect all literals of $C$ once and check if the new clause is not prime. If One clause is prime it follows that F is not prime.

I think the equivalence for the other direction is similarly . Assume the definition of Boros. Then if we consider the clause $C$ and drop an arbitrary literal we get $C_1$ which is not an implicate if $C$ is prime so $F\nrightarrow C_1$. Again we have oviously $C_1 \rightarrow C$ and by dropping any more arbitrary literals in $C_1$ to get $C_2$ we note $F\nrightarrow C_2 \rightarrow C_1$(otherwise $F\rightarrow C_2 \rightarrow C_1$ which is wrong since $C_1$ is no implicate). Since by dropping literals we can produce arbitrary sub-clauses one can follow that also all proper sub-clauses of C cant be prime otherwise $F\rightarrow C_2 \rightarrow C_1$ which is a contradiction. And Kiras definition follows.

Is my reasoning correct?

Answer 1

This equivalence is a somewhat folklore idea in papers about prime implicants. A small proof is presented in the "Definitions" section of this paper. The idea behind the equivalence is that, if $C$ is not a prime implicant for $\varphi$, then there is a proper subset $C'$ of $C$ (identifying clauses with the set of literals they force) such that $C'$ is an implicant of $\varphi$. But if this is the case, then you can fill $C'$ with the literals in $C \setminus C'$ until it has size $|C| - 1$, and thus, you obtain an implicant that is $C$ minus exactly one literal you "dropped". The other direction of the equivalence is trivial: if no proper subset of $C$ is an implicant, then dropping any literal of $C$ gives you something that is not an implicant.

I don't see the relation with Horn formulas, as the equivalence is about definitions for prime implicants of any formula.