Closed fblanqui closed 1 year ago
I guess so. Moreover Geoff will make sure that, in TPTP, symbols and axioms do not use the same names. There could also be name clashes between TPTP symbols/axioms and encoding symbols. This is not possible with the current encoding since it is using Unicode symbols while TPTP only accepts ASCII symbols (this may be a problem for dkcheck though).
It seems that Pierre Halmagrand add those "ax_" in the middle of some big commit, but without commenting why. Perhaps to avoid name clashes with Dedukti?