Reputation: 259
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
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