3 ms·
That's a very good point. I have been strongly influenced by Isabelle and Isar, which get a lot of things right. I think the future looks like this: The result
by practal 2y ago
That's a very good point. I have been strongly influenced by Isabelle and Isar, which get a lot of things right.
I think the future looks like this: The resulting text will be natural language (LLM powered), layering upon the actual formal logic. I think Abstraction Logic is actually best suited for this scenario, and I am designing Practal from scratch for it.