# Is it possible to encode contradictory horn clauses without goal clauses?

Intuitively, this seems impossible (because negation is forbidden in the head), but i am not sure.

A naive (and wrong) example is

p :- p


But, this just means

¬p or p


We can get the assignment p=true, so no contradiction.

Could you give me an example of contradictory horn clauses without goal clauses if it is possible (e.g. in propositional logic or predicate logic)? I did not find any explanation about this intuitive property of horn clauses on the internet.

Thanks.

• In logic programming, computation and query evaluation are performed by representing the negation of a problem to be solved as a goal clause. Solving the problem amounts to deriving a contradiction, which is represented by the empty clause (or "false")...Horn clause logic is equivalent in computational power to a universal Turing machine. as hinted here. So only goal clause can do RAA and your intuition is why Horn clauses are useful for knowledge representation as there's no subjunctive (negated) literal sentences allowed here. Commented Oct 29, 2021 at 17:36

If you only allow propositional letters p, q, r, ... and Horn clauses of the form q :- p₁, ..., pᵢ then what you are asking for is not possible: we may satisfy any such set of Horn clauses by setting all the propositional letters to true.
If you allow anything that is equivalent to false, then things get easy, becaue false is a Horn clause (with zero premises).