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