ChatGPT and Mark work together to solve a hard problem

[dr.mt...@gmail.com]

This was something I looked at in 2010 and did several times

in different ways, looking for the shortest cleanest version.

The task is to reduce Shen functions to logical formulae.

e.g. 

((factorial 0) = 1)
(all X ((~ (X = 0)) => ((factorial X) = (* X (factorial (- X 1))))))

is mechanically extracted from the factorial definition.  

Its a seriously hard problem and I did it with myself supplying

the blueprint and ChatGPT figuring out the bugs.   It is a tricky

program using both Shen Prolog and Shen in harness.  W.O.

ChatGPT I think I might not have finished this.

The technology has come a scary way in a year and I wonder

honestly what world our kids are going to inherit.  Seriously;

and I'm an ex-AI guy.

The program needs a correctness proof that the logical representation

captures the semantics properly.  Again this will be a joint AI/Mark

effort if it happens.

Mark