How can I implement `unfold` predicate?

General
1

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.

2

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

3

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.

4

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

5

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.

6

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.

7

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.

8

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 ?

10

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

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

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

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

16

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.

bratko
bratko843×1023 227 KB

1 Like
18

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

20

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.

21

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