0
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – cinch
    Commented Oct 29, 2021 at 17:36

1 Answer 1

Reset to default
1
$\begingroup$

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).

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks. I think it's a very good property of Horn clause, because it can rule out inconsistent knowledge by syntax. If someone gives us a lot of knowledge and if they use classical logic formulas to encode, there is no guarantee that no contradiction in them. $\endgroup$
    – chansey
    Commented Oct 29, 2021 at 9:42
  • $\begingroup$ I also noticed that even if negation (pure logic negation, not negation as failure) could be used in the body of definite clauses, there seems still no contradiction. However, those are no longer Horn clauses and it might lose some other good properties of Horn clause. There are seemingly some hierarchies for logic languages. $\endgroup$
    – chansey
    Commented Oct 29, 2021 at 9:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.