zer0kai
zer0kai

Reputation: 259

Check if a formula is a horn clause

I made a program in prolog with the operators ~(not), v(or) and ^(and). How can I check if a formula is a horn clause?

For example:

?- hclause((A ^ ~B) v (~A ^ C))
true.

Thanks in advance!

Upvotes: 0

Views: 426

Answers (1)

max66
max66

Reputation: 66230

Not sure to understand but... if you define ^ and v as binary operators and ~ as unary operator, by example

:- op(400,  fx, ~).
:- op(500, xfy, ^).
:- op(600, xfy, v).

the check of a correct formula should be automatic (giving error otherwise).

Take in count that operator definition is only "Syntactic sugar" and that, by example, A ^ B is an alternative version for ^(A, B).

If you want to see the real meaning of (A ^ ~B) v (~A ^ C) (with this definition for v, ^ and ~), you can use write_canonical/1, so with

write_canonical((A ^ ~B) v (~A ^ C)),

I obtain

v(^(_4,~(_7)),^(~(_4),_15))

Upvotes: 3

Related Questions