Work with logical functors in Prolog

Question

I want to have logical connectives like

not(X), conj(X, Y), some(Y, K). , and I want to be able to iterate over them.

So, for example, I want to be able to convert not (some (Y, K)) to all (Y, not (K)).

I do not want them to have any special meaning, I just want to work with logical formulas in this way.

What is the best way to do this?

Here is the actual line in my code:

 nnf(not(all(X, Y)) ,some(Z, W)) :- nnf(X, Z), nnf(not(Y), W). 

So, if I give it not(all(a,b)) , I want to return some (a, not (b)), but atm. I don't know how to get Prolog to handle not/1 and all/2 in this way.

Answer 1

There is no unique best way. It depends a little on your specific applications.

Your question essentially boils down to: how variables should be displayed in your setup. Ground term? This is a free representation of a variable (Prolog). Or directly using the Prolog variables.

I would prefer to create the first view first. Perhaps try v(Nr) with an Nr integer. Relatively frequent is '$VAR'(Nr) , which is also recognized by writeq/1 . But in the beginning I would stick with v/1 .

Answer 2

Check out the Thea project . He is developing the Prolog library for OWL2 ontology management. Perhaps they have already implemented the transformation of the normal form of negation.