# How can I implement `unfold` predicate?

Hello community,

I am trying to implement an `unfold` predicate which takes a propositional formula and returns one where the only logical operators are conjunction, disjunction and negation.

Code:

``````:- op(1060, yfx, <->).
:- op(1050, yfx, <-).
:- op(800, yfx, xor).
:- op(600, yfx, v).
:- op(400, yfx, &).
:- op(200, fy, ¬).

define((F xor G),  ¬ (F <-> G)).
define((F <-> G), (F -> G) & (F <- G)).
define((F <- G), (G -> F)).
define((F -> G), ¬ F v G).

% Base case: atomic formula
unfold(A, A) :- atom(A).
unfold(¬ A, NA) :- unfold(A, UA), define(UA, NA1), NA = ¬ NA1.
unfold(A & B, C) :- unfold(A, UA), unfold(B, UB), define(UA, C1), define(UB, C2), C = C1 & C2.
unfold(A v B, C) :- unfold(A, UA), unfold(B, UB), define(UA, C1), define(UB, C2), C = C1 v C2.
unfold(A xor B, C) :- unfold(A, UA), unfold(B, UB), define((UA xor UB), C).
unfold(A <-> B, C) :- unfold(A, UA), unfold(B, UB), define((UA <-> UB), C).
unfold(A <- B, C) :- unfold(A, UA), unfold(B, UB), define((UA <- UB), C).
unfold(A -> B, C) :- unfold(A, UA), unfold(B, UB), define((UA -> UB), C).
``````

However, that doesn’t work. At first I missed the base case, then I added it but I only get `false`. For example, this query should return:

``````-? unfold( p <-> q & ¬ r, G ).
G= ( ¬p v ¬q & ¬r) & ( ¬ (q & ¬ r) v p).
``````

Thank you for any guidance or help.

This sounds like you are trying to convert propositional formula to a normal form such as CNF, DNF or NNF.

Here is a ChatGPT prompt that should give you some help. Remember that ChatGPT is a LLM so expect hallucinations.

Create an SWI-Prolog program to convert a predicate formula (‘and’, ‘or’, ‘not’, ‘implication’ and ‘biconditional’) into a disjunctive normal form (‘and’, ‘or’ and ‘not’ only ) give some examples.

Prolog Programming for Artificial Intelligence (4th Edition) by Ivan Bratko (WorldCat )
Section 25.8 - A simple theorem prover as a pattern-directed program
which contains Figure 25.15 `Translating a propositional calculus formula into a set of (asserted) clauses.` on page 638

Thank you for your input. Tried that but ChatGPT is giving me errors. Does anything in my code incorrect, at a first glance ? I am wondering why I always get `false` despite it seems correct to my eyes.

By the way, thank you for that recommendation. I already have the book.

First of I am really bad with operators so take this more as something you should double check than believe it is true but the book is typically using `xfy` and you are using `yfx`.

If you want a more in-depth book but much more expensive.

“Handbook of Practical Logic and Automated Reasoning” by y John Harrison (WorldCat)
The book implements the logic of Prolog in OCaml and in Chapter 2 does what it seems you are seeking.
The books web page makes the OCaml available.

Thank you. I am glancing through it but unfortunately it is above my current level. Bratko section is useful, but I do not know how can I benefit from `translate` predicate and use it in my code.

It is a hard book to get through, some of us translated the OCaml to F# over a decade ago as an exercise so you really have to understand OCaml, parser combinators and the printing system up front to make head way. If you read the book at the end of each chapter are reference sections (`Further reading`) that are actually worthy even a decade latter because the logic has not changed.

It would help if we knew what your end goal is, I can only make guesses so far.

I appreciate your recommendation.

I would like to define a predicate which translates a propositional formula into another one where the only logical operators are conjunction, disjunction and negation.

So, for example:

``````-? unfold( p <-> q & ¬ r, G ).
G= ( ¬p v ¬q & ¬r) & ( ¬ (q & ¬ r) v p).
``````

Though, I think that result doesn’t fit into any of the normal forms, right ?

Thank you very much. I’ve updated the code. Now, unification occurs, though it still has to remove more operators:

``````:- op(1060, yfx, <->).
:- op(1050, yfx, <-).
:- op(800, xfy, xor).
:- op(600, xfy, v).
:- op(400, xfy, &).
:- op(200, fy, ¬).

define((F xor G),  ¬ (F <-> G)).
define((F <-> G), (F -> G) & (F <- G)).
define((F <- G), (G -> F)).
define((F -> G), ¬ F v G).

unfold(X, X) :- atom(X).
unfold(¬ X, ¬ X1) :- unfold( X, X1).
unfold(X & Y, X1 & Y1) :- unfold(X, X1), unfold(Y, Y1).
unfold(X v Y, X1 v Y1) :- unfold(X, X1), unfold(Y, Y1).
unfold( X <-> Y, Z) :- unfold(X, X1), unfold(Y, Y1), define(X1 <-> Y1, Z).
unfold( X -> Y, Z) :- unfold(X, X1), unfold(Y, Y1), define(X1 -> Y1, Z).
unfold( X <- Y, Z) :- unfold(X, X1), unfold(Y, Y1), define(X1 <- Y1, Z).
``````

Output:

``````?- unfold((p <-> q) & ¬ r, G).
G = ((p->q)&(p<-q))& ¬r.
``````

Thank you !

This is my new attempt, but I get the same output:

``````:- op(1060, yfx, <->).
:- op(1050, yfx, <-).
:- op(800, xfy, xor).
:- op(600, xfy, v).
:- op(400, xfy, &).
:- op(200, fy, ¬).

define((F xor G),  ¬ (F <-> G)).
define((F <-> G), (F -> G) & (F <- G)).
define((F <- G), (G -> F)).
define((F -> G), ¬ F v G).

unfold(X, X) :- atom(X).
unfold(¬ X, ¬ X1) :- unfold( X, X1).
unfold(X & Y, X1 & Y1) :- unfold(X, X1), unfold(Y, Y1).
unfold(X v Y, X1 v Y1) :- unfold(X, X1), unfold(Y, Y1).
unfold( X -> Y, ¬ X1 v Y1) :- unfold(X, X1), unfold(Y, Y1).
unfold( X <- Y, Z) :- unfold(X -> Y, Z).
unfold( X <-> Y, (X1 -> Y1) & (X1 <- Y1)) :- unfold(X, X1), unfold(Y, Y1).
unfold(X xor Y,  ¬ (X1 <-> Y1)) :- unfold(X, X1), unfold(Y, Y1).
``````

Try changing these as well, make them similar to the `(<-)/2` rule.

Currently the above rules do not call `unfold/2` with `(X1 -> Y1)` etc…, since
`(X1 -> Y1)` etc… is returned in the second argument of the `unfold/2` head. So
elimination stops again prematurely.

Last but not least, the `(<-)/2` rule itself needs also a little improvement.
I had a typo when I wrote it down, I edited my post.

1 Like

This is better, thank you. What do you think ?

``````:- op(1060, yfx, <->).
:- op(1050, yfx, <-).
:- op(800, yfx, xor).
:- op(600, yfx, v).
:- op(400, yfx, &).
:- op(200, fy, ¬).

unfold(X, X) :- atom(X).
unfold(¬ X, Z) :- unfold( X, X1), Z = ¬ X1.
unfold(X & Y, Z) :- unfold(X, X1), unfold(Y, Y1), Z = X1 & Y1.
unfold(X v Y, Z) :- unfold(X, X1), unfold(Y, Y1), Z = X1 v Y1.
unfold( X -> Y, Z1) :- unfold(X, X1), unfold(Y, Y1), Z = ¬ X1 v Y1, unfold(Z, Z1).
unfold( X <- Y, Z) :- unfold(Y -> X, Z).
unfold( X <-> Y, Z1) :- unfold(X, X1), unfold(Y, Y1), Z = (X1 -> Y1) & (X1 <- Y1), unfold(Z, Z1).
unfold(X xor Y, Z1) :- unfold(X, X1), unfold(Y, Y1), Z = ¬ (X1 <-> Y1), unfold(Z, Z1).
``````

Output:

``````?- unfold(p <-> q & ¬ r, G).
G = (¬p v q& ¬r)&(¬ (q& ¬r)v p).
``````

Expected output:

``````-? unfold( p <-> q & ¬ r, G ).
G= ( ¬p v ¬q & ¬r) & ( ¬ (q & ¬ r) v p).
``````

Yes, that would be ideal. Could you give me a hint ?

The book is quite useful, you can find some unfold/2
in there. The difference between Bratkos transform/1 and
the unfold/2 posted here, is as follows:

• The unfold/2 here: It calls unfold/2 first and then define/2,
I am refering to the version that was posted at the beginning of the thread.

• Bratkos translate/1: It does the translation the other way around.
It calls transform/2 (corresponds to define/2) first, and then translation/1 (corresponds to unfold/2).

See for yourself. If you replace the assert/1 by an output parameter,
this way you can make an unfold/2 that will eliminate everything. You
might also want to move the `(X v Y)` handling from transform/2 to translate/1

and omit the double negation, deMorgan and distribution laws, if you
want something more primitive, and only put elimination rules into transform/2.

1 Like

Basically you can think the problem is a classical rewriting
problem, and thus a solution is the transitive and subterm
closure of a simple rewriting relation:

``````F xor G  ~~>  ¬ (F <-> G).
F <-> G ~~>  (F -> G) & (F <- G).
F <- G ~~>  G -> F.
F -> G ~~>  ¬ F v G.
``````

So while `(~~>)/2` in the above defines a single step
of rewriting, the unfold/2 needs to do multiple steps.
For example to reduce `p xor q`, you will get `¬ (p <-> q)`.

But the `(<->)/2` in the single step result is not yet eliminated.
So in the end you need to program a transitive and subterm
closure. There are different ways to do that, its the

generic problem of term rewriting.

A term rewriting system (TRS ) is a rewriting system whose objects
are terms , which are expressions with nested sub-expressions.
https://en.wikipedia.org/wiki/Rewriting

1 Like

@j4n_bur53, I can’t tell you how much I appreciate all your help. I’ll digest your responses and suggested reading.

Some challenge is to do it without cut (!)/0. Bratkos solution has
still the disadvantage that it uses a cut (!)/0, so we might consider
it impure. Maybe the less pompous name for term rewriting is

macro expansion? This might explain why you chose `define/2`?

#define Directive (macro definition)
https://learn.microsoft.com/en-us/cpp/preprocessor/hash-define-directive-c-cpp

Lets spin the idea further, how about `unfold/2` simply knows which
operators have a `define/2` and does it by itself as follows, making optimal
use of first argument indexing (*), no cut (!)/0 involved:

``````:- op(1060, yfx, <->).
:- op(1050, yfx, <-).
:- op(800, yfx, xor).
:- op(600, yfx, v).
:- op(400, yfx, &).
:- op(200, fy, ¬).

unfold(A, A) :- atom(A).
/* Result should have ¬, & and v only, so go into subterms */
unfold(¬ A, ¬ UA) :- unfold(A, UA).
unfold(A & B, UA & UB) :- unfold(A, UA), unfold(B, UB).
unfold(A v B, UA v UB) :- unfold(A, UA), unfold(B, UB).
/* xor, <->, <- and -> have macro definitions */
unfold(A xor B, C) :- unfold(¬ (A <-> B), C).
unfold(A <-> B, C) :- unfold((A -> B) & (A <- B), C).
unfold(A <- B, C) :- unfold((B -> A), C).
unfold(A -> B, C) :- unfold(¬ A v B, C).
``````

Lets give it a try:

``````?- unfold( p <-> q & ¬ r, G ).
G = (¬p v q& ¬r)&(¬ (q& ¬r)v p).
``````

Disclaimer: The above is kind of context free term rewriting. Take the
example of conjunction `A & B`, once we have obtained `UA` and `UB` we
form `UA & UB`, and do not come back reconsidering `UA & UB` as a whole.

I guess this works fine for the example at hand, but doesn’t cover term
rewriting in general. So the above might not work anymore if you start
introducing double negation, deMorgan or distribution laws as found

in the Bratkov book and the translate/1 predicate there.

(*) The word standard in the below doesn’t mean ISO core standard:

Standard PROLOG Indexing
The standard PROLOG indexing method described in [War83], [GLLO85],
and [AK90] uses the first argument of each procedure for indexing.
https://www.dfki.uni-kl.de/~sintek/pa/section1_2_0_4.html

1 Like

Thank you so so much, @j4n_bur53.

It occurred to me how can I use `define`:

``````:- op(1060, yfx, <->).
:- op(1050, yfx, <-).
:- op(800, yfx, xor).
:- op(600, yfx, v).
:- op(400, yfx, &).
:- op(200, fy, ¬).

define((F xor G),  ¬ (F <-> G)).
define((F <- G), (G -> F)).
define((F -> G), ¬ F v G).
define((F <-> G), (F -> G) & (F <- G)).

unfold(A, A) :- atom(A).
/* Result should have ¬, & and v only, so go into subterms */
unfold(¬ A, ¬ UA) :- unfold(A, UA).
unfold(A & B, UA & UB) :- unfold(A, UA), unfold(B, UB).
unfold(A v B, UA v UB) :- unfold(A, UA), unfold(B, UB).
/* xor, <->, <- and -> have definitions */
unfold(X, C) :- define(X, X1), unfold(X1, C).
``````

Does recursion continue because I placed `define` before `unfold` ? In this way, works but I would like to know why, if possible.

Works also. But leaves a spurious choice point in SWI-Prolog:

``````?- unfold( p <-> q & ¬ r, G ).
G = (¬p v q& ¬r)&(¬ (q& ¬r)v p) ;
false.
``````

You see this since it prompts in the top-level, and you can type
semicolon `(;)` but there is no further solution.

1 Like