Understanding Bratko `translate` predicate

[unlocked2412]

As a follow-up to @EricGT and @j4n_bur53 recommendation, I am studying:

Figure 25.15 Translating a propositional calculus formula into a set of (asserted) clauses., page 638

Book: Prolog Programming for Artificial Intelligence (4th Edition) by Ivan Bratko

Goal:

Rewrite a propositional formula like: p => q => r using the translate predicate explained in the book.

Source code:

:- op( 100, fy, ~). % Negation
:- op( 110, xfy, &). %Conjunction
:- op( 120, xfy, v). % Disjunction
:- op( 130, xfy, =>). % Implication

translate( F & G) :- !, % Translate conjunctive formula
    translate( F), 
    translate( G).

translate( Formula) :- 
    transform( Formula, NewFormula), !, % Transformation step on Formula
    translate( NewFormula ).

translate(Formula):-           % No more trasnformation possible
    assert( clause( Formula )). 

% Transformation rules for propositional formulas

transform(~(~X), X).
transform( X => Y, ~X v Y).
transform(~ (X & Y), ~X v ~Y). 
transform(~ (X v Y), ~X & ~Y).
transform( X & Y v Z, (X v Z) & (Y v Z)). 
transform( X v Y & Z, (X v Y) & ( X v Z)). 
transform( X v Y, X1 v Y) :- % Transform subexpression
    transform( X, X1), !. 
transform( X v Y, X v Y1) :- % Transform subexpression
    transform( Y, Y1), !.
transform( ~ X, ~ X1 ) :- % Transform subexpression
    transform( X, X1).

However, I noticed translate/1 predicate has arity 1, so I can’t use it to unify a variable with the transformed expression.

• How can I use that code to rewrite an arbitrary formula like p => q => r ?

Thank you for any guidance.

[EricGT]

@unlocked2412

How can I use that code to rewrite an arbitrary formula like p => q => r ?

If you rewrite translate/2 as

translate(F0 & G0,F & G) :- !, % Translate conjunctive formula
    translate(F0,F), 
    translate(G0,G).

translate(Formula0,Forumula) :- 
    transform(Formula0,Formula1), !, % Transformation step on Formula
    translate(Formula1,Forumula).

translate(Formula,Formula). % Pass final formula back.

it should work or give you some idea. I did not run this and thus did not test it.

Notice the names are changed to the classic accumulator passing notation.

For a very simple example of accumulator passing see:

Learn Prolog Now! 5.3 Arithmetic and Lists

[unlocked2412]

Thank you so much ! Works great, so far.

Could you please explain what these definitions mean ? Why do I need ! cut operator ?

transform( X v Y, X1 v Y) :- % Transform subexpression
    transform( X, X1), !. 
transform( X v Y, X v Y1) :- % Transform subexpression
    transform( Y, Y1), !.

and give any tips to learn prolog code like this one ? How do you read it ?

[EricGT]

@unlocked2412

Could you please explain what these definitions mean ? Why do I need ! cut operator ?

give any tips to learn prolog code like this one ? How do you read it ?

I am grateful you are willing to learn Prolog, are willing to accept advise and change course when suggested, and looking at the details, however this site is not for teaching Prolog.

Options

• Some users here will help more than others so you can ask but don’t always expect a reply.
• You also have the Bratko book which is still relevant at your level and worth taking a month or two to work through. Be advised that the book does not use append/3 but instead uses conc/3. Do yourself a favor and use append/3 when the book uses conc/3. Don’t believe me, check the books index at the back.
• For simple questions such as yours ChatGPT is not bad, it is also not great, but it is good at summarizing much of the information from its training data into coherent replies, however you do have to know Prolog to know when it is wrong or test out everything it tells you to know when it is wrong or hallucinating, which I too have to do for some things, e.g. popcount.
• See: Useful Prolog references

Feel free to ask your own questions and post what you learn along the way, I am sure others will read and learn from what you post.

[unlocked2412]

Thank you for all the advice. One question, if I may:

do you understand why the following two lines are used:

transform( X v Y, X1 v Y) :- % Transform subexpression
    transform( X, X1), !. 
transform( X v Y, X v Y1) :- % Transform subexpression
    transform( Y, Y1), !.

instead of:

transform( X v Y, X1 v Y1) :- % Transform subexpression
    transform( X, X1),
    transform( Y, Y1).

From my experience in other languages, this is what I would expect, but perhaps there is a Prolog detail I do not know. I assume the latter would be true, since I am just starting my Prolog journey.

In my tests, they behave differently.

[EricGT]

@unlocked2412

do you understand why the following two lines are used:

instead of:

Without checking I would speculate that as two rules either or both can be skipped, e.g. if a rule is not activated then the code will complete. With them combined into one rule if the first pattern did not need to be transformed then it would fail and if the second needed to be transformed it would not and thus an invalid result.

In other words as two separate clause (rules) the code works like an or but together in one clause (rule) they work as an and, the , at the end of transform( X, X1), is the and operator (,/2).

[unlocked2412]

Thank you so much.

@EricGT

With them combined into one rule if the first pattern did not need to be transformed then it would fail

Could you clarify what do you mean by “if the first pattern did not need to be transformed” ?

[unlocked2412]

@unlocked2412

@EricGT

With them combined into one rule if the first pattern did not need to be transformed then it would fail

Could you clarify what do you mean by “if the first pattern did not need to be transformed” ?

If I understand correctly, in this case:

transform(p v (p => (q => r)), G).

The left hand operand p cannot be further transformed, since it doesn’t match any of the facts or rules in the database, i.e, doesn’t match the patterns:

~(~X)
X => Y
~ (X v Y)
...

Is that right ?

So, if that is the second rule:

transform( X v Y, X v Y1) :- % Transform subexpression
    transform( Y, Y1).

is required in order to transform the right hand operand.

I come from a Haskell background, so this seems some form of pattern matching.

[EricGT]

@unlocked2412

Is that right ?

Sounds correct. Again I am not checking this by writing code and running it.

@unlocked2412

seems some form of pattern matching

It is syntactic unification. You really haven’t read any of the Bratko book have you?

Perhaps this page will help you

ChatGPT prompts - Prolog - Basics

There are several Wiki pages in sequence of ChatGPT starting here.

LLM (Large Language Model) such as ChatGPT prompts related to Prolog

[unlocked2412]

@EricGT

It is syntactic unification. You really haven’t read any of the Bratko book have you?

Thank you. I have searched the book for “pattern matching” but the results weren’t relevant. I have read some chapters of Clocksin in the past.

@EricGT

ChatGPT prompts - Prolog - Basics

There are several Wiki pages in sequence of ChatGPT starting here.

LLM (Large Language Model) such as ChatGPT prompts related to Prolog

Thank you for doing those wiki pages.

[EricGT]

@unlocked2412

I come from a Haskell background

Have you tried using ChatGPT or such to convert Prolog to Haskell or Haskell to Prolog?

I have not tried this using Prolog with Haskell but I do find that using ChatGPT to translate some code from one programming language to anther will at times help in understanding the one you don’t know.

[unlocked2412]

@EricGT

Have you tried using ChatGPT or such to convert Prolog to Haskell or Haskell to Prolog?

I didn’t try that. Thank you for the suggestion.

I’ve started using ChatGPT and so far it’s helping. However, I tried to extend the example from Bratko book, and ChatGPT gave me a code that doesn’t work nor I don’t know how to fix.

I said to ChatGPT:

Using the following Prolog code:
:- op(1060, yfx, <->). 
:- op(1050, yfx, <-). 
:- op(800, yfx, xor).
:- op(600, yfx, v).  
:- op(400, yfx, &). 
:- op(200, fy, ¬).

% Exercise 1

unfold(F0 & G0,F & G) :- !, % Translate conjunctive formula
    unfold(F0,F),
    unfold(G0,G).

unfold(Formula0,Formula) :- 
    define(Formula0,Formula1), !, % Transformation step on Formula
    unfold(Formula1,Formula).

unfold( X v Y, X1 v Y) :- % Transform subexpression
    unfold( X, X1), !.  
unfold( X v Y, X v Y1) :- % Transform subexpression
    unfold( Y, Y1), !.

unfold(Formula,Formula). % Pass final formula back.

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

implement a `tab/2` predicate which implements a semantic table algorithm, and returns as many open branches as it founds given any propositional formula. If that formula is inconsistent, return false

ChatGPT response:

Expand disclosure triangle to see "prolog" source

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

% Exercise 1

unfold(F0 & G0,F & G) :- !, % Translate conjunctive formula
    unfold(F0,F),
    unfold(G0,G).

unfold(Formula0,Formula) :- 
    define(Formula0,Formula1), !, % Transformation step on Formula
    unfold(Formula1,Formula).

unfold( X v Y, X1 v Y) :- % Transform subexpression
    unfold( X, X1), !.  
unfold( X v Y, X v Y1) :- % Transform subexpression
    unfold( Y, Y1), !.

unfold(Formula,Formula). % Pass final formula back.

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

% Define the semantic table algorithm
tab(Formula, Branches) :-
    unfold(Formula, Formula1), % Transform the formula
    propagate(Formula1, [], Branches). % Propagate the formula through the table

% Propagate the formula through the table
propagate([], Branches, Branches). % Base case: no more formulas to propagate
propagate([Formula | Rest], Branches, Result) :-
    (inconsistent(Formula) -> % If the formula is inconsistent
        Result = false % Return false
    ;
        split(Formula, Left, Right), % Split the formula into left and right branches
        append(Rest, Left, NewFormulas), % Add the left branch to the remaining formulas
        append(Rest, Right, NewFormulas1), % Add the right branch to the remaining formulas
        propagate(NewFormulas, Branches, Branches1), % Propagate the remaining formulas with the current branches
        propagate(NewFormulas1, Branches1, Result) % Propagate the remaining formulas with the updated branches
    ).

% Split a formula into left and right branches
split((F & G), [F, G], []). % Conjunction: add F and G as separate branches
split((F v G), [], [F, G]). % Disjunction: add F and G as separate branches
split((F <-> G), [(F -> G), (G -> F)], []). % Biconditional: add (F -> G) and (G -> F) as separate branches
split((F -> G), [(¬ F), G], []). % Implication: add (¬ F) and G as separate branches
split((F <- G), [F, (¬ G)], []). % Reverse implication: add F and (¬ G) as separate branches
split((F xor G), [(¬ (F <-> G))], []). % Exclusive disjunction: add (¬ (F <-> G)) as a separate branch
split(¬ (F & G), [¬ F], [¬ G]). % Negation of conjunction: add ¬ F and ¬ G as separate branches
split(¬ (F v G), [(¬ F) & (¬ G)], []). % Negation of disjunction: add (¬ F) & (¬ G) as a separate branch
split(¬ (F <-> G), [(F & (¬ G)) v ((¬ F) & G)], []). % Negation of biconditional: add (F & (¬ G)) v ((¬ F) & G) as a separate branch
split(¬ (F -> G), [F, ¬ G], []). % Negation of implication: add F and ¬ G as separate branches
split(¬ (F <- G), [(¬ F) v G], []). % Negation of reverse implication: add (¬ F) v G as a separate branch
split(¬ (F xor G), [(F & G) v ((¬ F) & (¬ G))], []). % Negation of exclusive disjunction: add (F & G) v ((¬ F) & (¬ G)) as a separate branch
split(Formula, [Formula], []). % Base case: single formula is a branch

% Check if a formula is inconsistent
inconsistent(Formula) :-
    member(Formula, [false, ¬ true, (F & ¬ F), (F & (¬ F)) v ((¬ F) & G), (F & (¬ F)) v ((¬ F) & ¬ G),
                      (F v (¬ F)), (¬ (F <-> F)), (¬ (F -> F)), (¬ (F <- F)), (¬ (F xor F))]).

Output:

?- tab(a -> ¬ (b -> c), R).
false

However, I would expect:

tab(a -> ¬ (b -> c), R).
R=[¬a];
R= [b, ¬ c]; 
false

I wouldn’t know how to fix this, but nonetheless impressive what it can do so far.

[EricGT]

@unlocked2412

ChatGPT gave me a code that doesn’t work nor I don’t know how to fix.

One should not expect ChatGPT or any LLM to correctly generate Prolog code. After hundreds of Prolog code prompts of ChatGPT and having seen a lot of the different Prolog code online, as many others note about training data, if it is not in the training data then don’t expect similar for the output and that garbage in will lead to garbage out. So while I do find that ChatGPT is good at giving me a compass direction to head or a general idea of what the code should look like I always test it. It often fails the make. However if one has seen and used lots of Prolog code it does make it easier to find the problems and quickly decide if one should abandon the ChatGPT generated code or try to fix the issues.

As I don’t understand what you seek by reading the prompt I can’t judge the code.

Have you tried converting the Bratko code to Haskell, then having ChatGPT extend it and get it working using your knowledge of Haskell and then convert that back to Prolog?

You really need to take the time to work through the first several chapters of the book because when you get stuck you then have to learn how to debug the Prolog and you can come back to your problem. You keep trying to skip the basics and we are not here to teach them to you.

[unlocked2412]

Thank you for your valuable guidance ! I just tried to post what I’ve found in my first use of ChatGPT.

I’ll take note of your suggestions and apply them.

[unlocked2412]

@EricGT

As I don’t understand what you seek by reading the prompt I can’t judge the code.

I am trying to find out whether a propositional formula built from the logical connectives defined in the code is inconsistent. If it is not, should return open branches, otherwise returns false.

Is the problem, at least, clear enough for an expert Prolog programmer than yourself ?

[EricGT]

@unlocked2412

an expert Prolog programmer than yourself

That was funny because I am not a Prolog expert. Jan W. and others consistently shows me my mistakes for which I am grateful. I do try to not ask the same question again and sometimes its months of revisiting the advise before the advise makes sense but learning from ones mistakes is one of the fastest ways to learn so as you I will ask when stuck but that has become less frequent.

I really have no idea where you are headed in the long term. I know functional languages like Haskell eat and breath fold but this is not Haskell, it is Prolog and relationships are king. You really need to do a context switch and dump Haskell and since the new context is empty, learn from the book to understand what a relationship means.

---

EDIT

When it comes to naming predicates if a verb sounds correct then often the thinking is wrong.
See: Declarative reading

[unlocked2412]

@EricGT

learn from the book to understand what a relationship means.

Great ! Thank you.

At least I know the problem is not clear, so that means I have to study more to:

• first clarify the problem, and
• have a first outline of the solution.

[unlocked2412]

For the sake of completeness, I leave here the complete Bratko example I used to build on top. Before, I made the mistake of using different names. Note translate has one extra argument compared to the book:

translate(F0 & G0,F & G) :- !, % Translate conjunctive formula
    translate(F0,F), 
    translate(G0,G).

translate(Formula0,Forumula) :- 
    transform(Formula0,Formula1), !, % Transformation step on Formula
    translate(Formula1,Forumula).

translate(Formula,Formula). 

Prolog source code:

:- op( 100, fy, ~). % Negation
:- op( 110, xfy, &). % Conjunction
:- op( 120, xfy, v). % Disjunction
:- op( 130, xfy, =>). % Implication

translate(F0 & G0,F & G) :- !, % Translate conjunctive formula
    translate(F0,F), 
    translate(G0,G).

translate(Formula0,Formula) :- 
    transform(Formula0,Formula1), !, % Transformation step on Formula
    translate(Formula1,Formula).

translate(Formula,Formula). % Pass final formula back.

% Transformation rules for propositional formulas
transform(~(~X), X).
transform( X => Y, ~X v Y).
transform(~ (X & Y), ~X v ~Y). 
transform(~ (X v Y), ~X & ~Y).
transform( X & Y v Z, (X v Z) & (Y v Z)). 
transform( X v Y & Z, (X v Y) & ( X v Z)). 
transform( X v Y, X1 v Y) :- % Transform subexpression
    transform( X, X1), !.  
transform( X v Y, X v Y1) :- % Transform subexpression
    transform( Y, Y1), !.
transform( ~ X, ~ X1 ) :- % Transform subexpression
    transform( X, X1).

The question asked to ChatGPT:

Using the following Prolog code:

Expand disclosure triangle to see "prolog" source

:- op( 100, fy, ~). % Negation
:- op( 110, xfy, &). %Conjunction
:- op( 120, xfy, v). % Disjunction
:- op( 130, xfy, =>). % Implication

translate(F0 & G0,F & G) :- !, % Translate conjunctive formula
    translate(F0,F), 
    translate(G0,G).

translate(Formula0,Formula) :- 
    transform(Formula0,Formula1), !, % Transformation step on Formula
    translate(Formula1,Formula).

translate(Formula,Formula). % Pass final formula back.

% Transformation rules for propositional formulas
transform(~(~X), X).
transform( X => Y, ~X v Y).
transform(~ (X & Y), ~X v ~Y). 
transform(~ (X v Y), ~X & ~Y).
transform( X & Y v Z, (X v Z) & (Y v Z)). 
transform( X v Y & Z, (X v Y) & ( X v Z)). 
transform( X v Y, X1 v Y) :- % Transform subexpression
    transform( X, X1), !.  
transform( X v Y, X v Y1) :- % Transform subexpression
    transform( Y, Y1), !.
transform( ~ X, ~ X1 ) :- % Transform subexpression
    transform( X, X1).

Implement a tab/2 predicate which implements a semantic table algorithm, and returns as many open branches as it founds given any propositional formula. If that formula is inconsistent, return false

The response from ChatGPT

Expand disclosure triangle to see "prolog" source

:- op( 100, fy, ~). % Negation
:- op( 110, xfy, &). %Conjunction
:- op( 120, xfy, v). % Disjunction
:- op( 130, xfy, =>). % Implication

% Main predicate to call the semantic table algorithm
tab(Formula, Branches) :-
    translate(Formula, TranslatedFormula),
    create_initial_table(Table),
    expand_table(Table, TranslatedFormula, NewTable),
    check_consistency(NewTable, Branches).

% Predicate to create an initial table with a single row containing the formula
create_initial_table([(1, Formula)]) :-
    !, % Cut to prevent backtracking
    Formula.

% Predicate to expand the table by adding new rows based on the formula
expand_table(Table, Formulas, NewTable) :-
    findall((I, F), (member((I, F), Table), expand_formula(F, Formulas)), NewFormulas),
    subtract(NewFormulas, Table, FormulasToAdd),
    append(Table, FormulasToAdd, NewTable).

% Predicate to expand a formula based on its type
expand_formula(~ F, [F]).
expand_formula(F & G, [F, G]).
expand_formula(F v G, [F, G]).
expand_formula(F => G, [~ F, G]).

% Predicate to check the consistency of the table and compute open branches
check_consistency([], []).
check_consistency([(I, F) | T], Branches) :-
    (satisfiable(F) ->
        check_consistency(T, Branches)
    ;
        Branches = [I | RestBranches],
        check_consistency(T, RestBranches)
    ).

% Predicate to check if a formula is satisfiable
satisfiable(Formula) :-
    \+ unsatisfiable(Formula).

% Predicate to check if a formula is unsatisfiable
unsatisfiable(Formula) :-
    \+ satisfiable(Formula).

% Predicate to translate a formula using the given transformation rules
translate(F0 & G0, F & G) :- !,
    translate(F0, F),
    translate(G0, G).
translate(Formula0, Formula) :-
    transform(Formula0, Formula1), !,
    translate(Formula1, Formula).
translate(Formula, Formula).

% Predicate to apply transformation rules on propositional formulas
transform(~ (~X), X).
transform(X => Y, ~X v Y).
transform(~ (X & Y), ~X v ~Y).
transform(~ (X v Y), ~X & ~Y).
transform(X & Y v Z, (X v Z) & (Y v Z)).
transform(X v Y & Z, (X v Y) & (X v Z)).
transform(X v Y, X1 v Y) :-
    transform(X, X1), !.
transform(X v Y, X v Y1) :-
    transform(Y, Y1), !.
transform(~ X, ~ X1) :-
    transform(X, X1).

[EricGT]

FYI about using Discourse Hide Details (the triangle that expands a section) which is found in the Discourse editor toolbar

under the gear icon

At present

• Those sections are not searched by Discourse search (the magnifying glass in the upper right).

• Those sections are not passed along to search engines. Since an LLM completion will often contain invalid code or hallucinations, putting those results in Hide Details keeps others from easily finding it, namely those learning Prolog who do not know it is wrong. Hopefully by using Hide Details it will also keep the code from being included in training sets for future AI.

[unlocked2412]

Thank you for the information. So, I will continue using Hide Details if I happen to post some ChatGPT response.

@EricGT

When it comes to naming predicates if a verb sounds correct then often the thinking is wrong.
See: Declarative reading

By the way, thank you for this resource. It has helped me. I have read it from top to bottom

When it comes to naming predicates if a verb sounds correct then often the thinking is wrong.

This is interesting. Could you please clarify this ? Could you give an example ?