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?