Hi, In an old paper (esslli '96) Thorsten says: ...Often relations are defined inductively, i.e. as the least relation satisfying a certain property. In many cases (where the property is given as generalised Horn clauses) we can translate this into an inductively defined family...
This seems right, but I have no clue (1) if he means automatically? (2) how to prove it. I'm refering to the translation (but I am sending this from home through mailx and I can't go back to the previous line!). BTW, It's in Sec 3.5 first paragraph. Can anyone clarify or point me to the right direction (paper)? Thanks, Laszlo
